Filter base (source code)

= Filter base
{title2=$\forall F,G\in\mathcal F\ \exists H\in\mathcal F\ (H\subseteq F\cap G)$}

A <filter base> is a nonempty family of nonempty <subsets> directed under reverse inclusion. Its upward closure is a <filter>[proper filter]. Every <finite intersection> contains a base member, so it has the <finite intersection property>.