Chain is Directed

Theorem

Let $\struct {S, \preceq}$ be an ordered set.

Let $C$ be a non-empty chain of $S$.

Then $C$ is directed.

Proof

Let $x, y \in C$.

By definition of connected relation:

$x \preceq y$ or $y \preceq x$

Without loss of generality, suppose that

$x \preceq y$

Define $z = y$.

Thus by definition of reflexivity

$x \preceq z$ and $y \preceq z$

Hence $C$ is directed.

$\blacksquare$

Sources

• Mizar article WAYBEL_6:condreg 1