ThmDex – An index of mathematical definitions, results, and conjectures.
P809
Let $m$ be a minimal element in $P$ and let $x \in X$ such that $x \neq m$. Since $P$ is an ordered set, either $x \preceq m$ or $m \preceq x$. Since $m$ is a minimal element, $x \preceq m$ can not hold, so $m \preceq x$ must hold. Furthermore, $P$ being an ordered set necessitates that $m \preceq m$. Since $x \in X$ was arbitrary, this establishes that $m$ is a minimum element. $\square$