An D548: Ordered pair $P_E = (E, {\preceq}_E)$ is a chain in $P$ if and only if
| (1) | $E \subseteq X$ | (D78: Subset) |
| (2) | \begin{equation} {\preceq}_E = {\preceq} \cap (E \times E) \end{equation} | (D333: Binary subrelation) |
| (3) | $P_E$ is an D1707: Ordered set |