\begin{definition}[Definition:Filter on Set/Definition 1]
Let $S$ be a set.
Let $\powerset S$ denote the power set of $S$.
A '''filter on $S$''' (or '''filter of $S$''') is a set $\FF \subset \powerset S$ which satisfies the following conditions:
{{begin-axiom}}
{{axiom | n = \text F 1
        | m = S \in \FF
}}
{{axiom | n = \text F 2
        | m = \O \notin \FF
}}
{{axiom | n = \text F 3
        | m = U, V \in \FF \implies U \cap V \in \FF
}}
{{axiom | n = \text F 4
        | m = \forall U \in \FF: U \subseteq V \subseteq S \implies V \in \FF
}}
{{end-axiom}}
\end{definition}