Top in Filter
Let $F$ be a filter on $S$.
Then $\top \in F$
where $\top$ denotes the greatest element of $S$.
By definition of filter in ordered set:
By definition of non-empty set:
- $\exists x: x \in F$
By definition of greatest element:
- $x \preceq \top$
Thus by definition of upper set:
- $\top \in F$
- Mizar article WAYBEL_4:22