Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$

Remark 4.7.1.18. In the situation of Corollary 4.7.1.17, suppose that conditions $(1)$ and $(2)$ are both satisfied: that is, there exist initial segment embeddings $f: S \hookrightarrow T$ and $g: T \hookrightarrow S$. Then $g \circ f$ is an initial segment embedding of $S$ into itself, and therefore coincides with $\operatorname{id}_{S}$ (Corollary 4.7.1.16). The same argument shows that $f \circ g = \operatorname{id}_{T}$, so that $f$ and $g$ are mutually inverse bijections. In particular, $S$ and $T$ have the same order type.