Infimum is Product in Order Category

Theorem

Let $\mathbf P$ be an order category whose ordering is $\preceq$.

Let $p, q \in \mathbf P_0$, and suppose that they have some infimum $r = \inf \set {p, q}$.

Then $r$ is a binary product of $p$ and $q$ in $\mathbf P$.

Suppose that there are morphisms $l \to p$ and $l \to q$ in $\mathbf P$.

That is to say, suppose $l \preceq p$ and $l \preceq q$.

Then $l$ is a lower bound for $\set {p, q}$.

By definition of infimum, we then have:

$l \preceq r = \inf \set {p, q}$

By definition of $\mathbf P$ as an order category, this means there is a morphism:

$l \to r$

By definition of $\mathbf P$, this morphism is necessarily unique.

Thus $r$ satisfies the UMP for the binary product of $p$ and $q$.

The result follows.

$\blacksquare$