(0)

\(f\)は順序を保つ単射なので任意の\(a,b\in X\)に対し、
\[ \left(a\preceq b\rightarrow f\left(a\right)\preceq f\left(b\right)\right)\land\left(a\ne b\rightarrow f\left(a\right)\ne f\left(b\right)\right) \] が成り立つので、
\begin{align*} a\precneqq b & \Rightarrow a\preceq b\land a\ne b\\ & \Rightarrow a\preceq b\land f\left(a\right)\ne f\left(b\right)\\ & \Rightarrow f\left(a\right)\preceq f\left(b\right)\land f\left(a\right)\ne f\left(b\right)\\ & \Leftrightarrow f\left(a\right)\precneqq f\left(b\right) \end{align*} となる。

(0)-2

\(f\)は順序を保つ単射なので任意の\(a,b\in X\)に対し、
\begin{align*} \left(a\preceq b\rightarrow f\left(a\right)\preceq f\left(b\right)\right)\land\left(a\ne b\rightarrow f\left(a\right)\ne f\left(b\right)\right) & \Leftrightarrow\left(\lnot\left(a\preceq b\right)\lor f\left(a\right)\preceq f\left(b\right)\right)\land\left(\lnot\left(a=b\right)\lor f\left(a\right)\ne f\left(b\right)\right)\\ & \Leftrightarrow\left(\lnot\left(a\preceq b\right)\land\left(\lnot\left(a=b\right)\lor f\left(a\right)\ne f\left(b\right)\right)\right)\lor\left(f\left(a\right)\preceq f\left(b\right)\land\left(\lnot\left(a=b\right)\lor f\left(a\right)\ne f\left(b\right)\right)\right)\\ & \Rightarrow\lnot\left(a\preceq b\right)\lor\left(f\left(a\right)\preceq f\left(b\right)\land\left(\lnot\left(a=b\right)\lor f\left(a\right)\ne f\left(b\right)\right)\right)\\ & \Leftrightarrow\lnot\left(a\preceq b\right)\lor\left(f\left(a\right)\preceq f\left(b\right)\land\lnot\left(a=b\right)\right)\lor\left(f\left(a\right)\preceq f\left(b\right)\land f\left(a\right)\ne f\left(b\right)\right)\\ & \Rightarrow\lnot\left(a\preceq b\right)\lor\lnot\left(a=b\right)\lor\left(f\left(a\right)\preceq f\left(b\right)\land f\left(a\right)\ne f\left(b\right)\right)\\ & \Leftrightarrow\lnot\left(a\preceq b\land a=b\right)\lor\left(f\left(a\right)\preceq f\left(b\right)\land f\left(a\right)\ne f\left(b\right)\right)\\ & \Leftrightarrow\lnot\left(a\precneqq b\right)\lor\left(f\left(a\right)\precneqq f\left(b\right)\right)\\ & \Leftrightarrow a\precneqq b\rightarrow f\left(a\right)\precneqq f\left(b\right) \end{align*} これより、\(a\precneqq b\rightarrow f\left(a\right)\precneqq f\left(b\right)\)が成り立つ。