全順序集合の後続元は存在すれば一意

$ \forall x\in X\forall s,t\in X: x\lessdot s\land x\lessdot t\implies s=t

証明

$ \forall x\in X\forall s,t\in X:

$ \begin{dcases}x\lessdot s\\x\lessdot t\end{dcases}

$ \iff\begin{dcases}x<s\\x<t\\\forall z\in X:x<z\implies z\nless s\\\forall z\in X:x<z\implies z\nless t\end{dcases}

$ \implies\begin{dcases}t\nless s\\s\nless t\end{dcases}

$ \iff\begin{dcases}t\le s\implies t=s\\s\le t\implies s=t\end{dcases}

$ \iff(t\le s\lor s\le t\implies t=s)

$ \implies t=s

$ \underline{\therefore\forall x\in X\forall s,t\in X: x\lessdot s\land x\lessdot t\implies s=t\quad}_\blacksquare