ThmDex – An index of mathematical definitions, results, and conjectures.
Result R1077 on D668: Maximum element
Maximum element is unique
Formulation 0
Let $P = (X, {\preceq})$ be a D1103: Partially ordered set such that
(i) $X \neq \emptyset$
Let $a, b \in X$ each be a D2218: Set element in $X$ such that
(i) \begin{equation} \forall \, x \in X : x \preceq a \end{equation}
(ii) \begin{equation} \forall \, x \in X : x \preceq b \end{equation}
Then \begin{equation} a = b \end{equation}
Proofs
Proof 0
Let $P = (X, {\preceq})$ be a D1103: Partially ordered set such that
(i) $X \neq \emptyset$
Let $a, b \in X$ each be a D2218: Set element in $X$ such that
(i) \begin{equation} \forall \, x \in X : x \preceq a \end{equation}
(ii) \begin{equation} \forall \, x \in X : x \preceq b \end{equation}
By hypothesis, $b \preceq a$ and $a \preceq b$. A D286: Partial ordering relation is, particularly, an D289: Antisymmetric binary relation and therefore $a = b$. $\square$