Dual Ordered Set is Ordered Set

Theorem

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

Then its dual, $P^{-1} = \struct {S, \succeq}$, is also an ordered set.

Proof

Immediate from Dual Ordering is Ordering.

$\blacksquare$

Sources

• Mizar article YELLOW_7:5