Let $P = (X, {\preceq})$ be a D1707: Ordered set.
Let $\mathsf{Minimal}$ be the D4462: Set of minimal elements in $P$.
Let $\mathsf{Minimum}$ be the D4463: Set of minimum elements in $P$.

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$