Top in Filter

Theorem

Let $\struct {S, \preceq}$ be a bounded above ordered set.

Let $F$ be a filter on $S$.

Then $\top \in F$

where $\top$ denotes the greatest element of $S$.

Proof

By definition of filter in ordered set:

$F$ is non-empty and upper.

By definition of non-empty set:

$\exists x: x \in F$

By definition of greatest element:

$x \preceq \top$

Thus by definition of upper section:

$\top \in F$

$\blacksquare$

Sources

• Mizar article WAYBEL_4:22