\begin{definition}[Definition:Filter]
Let $\struct {S, \preccurlyeq}$ be an ordered set.
A '''filter of $\struct {S, \preccurlyeq}$''' (or a '''filter on $\struct {S, \preccurlyeq}$''') is a subset $\FF \subseteq S$ which satisfies the following conditions:
{{begin-axiom}}
{{axiom | n = 1
        | m = \FF \ne \O
}}
{{axiom | n = 2
        | m = x, y \in \FF \implies \exists z \in \FF: z \preccurlyeq x, z \preccurlyeq y
}}
{{axiom | n = 3
        | m = \forall x \in \FF: \forall y \in S: x \preccurlyeq y \implies y \in \FF
}}
{{end-axiom}}
\end{definition}