Singleton is Chain

Theorem

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

Let $x \in S$.

Then $\set x$ is a chain of $\struct {S, \preceq}$.

Proof

It suffices to prove that

$\set x$ is connected

Let $y, z \in \set x$.

By definition of singleton:

$y = x$ and $z = x$

By definition of reflexivity;

$y \preceq z$

Thus

$y \preceq z$ or $z \preceq y$

$\blacksquare$

Sources

• Mizar article ORDERS_2:8