Kerodon

Proof. For each element $s \in S$, let $S_{\leq s}$ denote the initial segment $\{ s' \in S: s' \leq s \} $. Let $S_0 \subseteq S$ denote the collection of elements $s \in S$ for which there exists an initial segment embedding $f_{\leq s}: S_{\leq s} \hookrightarrow T$. Note that, if this condition is satisfied, then the morphism $f_{\leq s}$ is uniquely determined (Corollary 4.7.1.15). Moreover, if $s' \leq s$, then composite map $S_{\leq s'} \subseteq S_{\leq s} \xrightarrow { f_{\leq s} } T$ is also an initial segment embedding; it follows that $s'$ belongs to $S_0$, and $f|_{\leq s'}$ is the restriction of $f|_{\leq s}$ to $S_{\leq s'}$. Consequently, the construction $s \mapsto f_ s(s)$ determines a function $f: S_0 \rightarrow T$, which is an isomorphism of $S_0$ with an initial segment $T_0 \subseteq T$. If $S_0 = S$, then $f$ is an initial segment embedding from $S$ to $T$. If $T_0 = T$, then $g = f^{-1}$ is an initial segment embedding from $T$ to $S$. Assume that neither of these conditions is satisfied: that is, the sets $S \setminus S_0$ and $T \setminus T_0$ are both nonempty. Let $s$ be a least element of $S \setminus S_0$, and let $t$ be a least element of $T \setminus T_0$. Then $f$ extends uniquely to an initial segment embedding

The existence of $f_{\leq s}$ shows that $s$ belongs to $S_0$, which is a contradiction. $\square$