Filtered iff Directed in Dual Ordered Set

Theorem

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

Let $\struct {S, \preceq_2}$ be a dual ordered set of $\struct {S, \preceq_1}$

Let $X \subseteq S$.

Then:

$X$ is filtered in $\struct {S, \preceq_1}$

if and only if:

$X$ is directed in $\struct {S, \preceq_2}$

Proof

By Dual of Dual Ordering:

$\struct {S, \preceq_1}$ is the dual of $\struct {S, \preceq_2}$.

Thus by Directed iff Filtered in Dual Ordered Set:

$X$ is filtered in $\struct {S, \preceq_1}$

if and only if:

$X$ is directed in $\struct {S, \preceq_2}$.

$\blacksquare$

Sources

• Mizar article YELLOW_7:27