Solution (source code)

= Solution

A <filter base> on a <set> $X$ is a nonempty family $\mathcal F$ of nonempty <subsets> such that for every $F,G\in\mathcal F$ there is $H\in\mathcal F$ with $H\subseteq F\cap G$. Repeated application gives a member contained in any specified <finite intersection>. In particular every <finite intersection> is nonempty, so the family has the <finite intersection property>. Its upward closure $\{A\subseteq X:\exists F\in\mathcal F, F\subseteq A\}$ is the corresponding <filter>[proper filter].