Dual of Preordered Set is Preordered Set

Theorem

Let $P = \struct {S, \preceq}$ be a preordered set.

Then dual of $P$, $P^{-1} = \struct {S, \succeq}$ is also a preordered set.

This needs considerable tedious hard slog to complete it. In particular: Dual Ordered Set $\ne$ Dual Preordered Set To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Finish}} from the code. If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.

Proof

By Inverse of Reflexive Relation is Reflexive:

$\succeq$ is reflexive.

By Inverse of Transitive Relation is Transitive:

$\succeq$ is transitive.

Hence $\succeq$ is a preordering.

$\blacksquare$

Sources

• Mizar article YELLOW_7:4

• Mizar article YELLOW_7:6