Membership in a free filter is detected by its ultrafilter extensions (source code)

= Membership in a free filter is detected by its ultrafilter extensions

For a <free filter> $F$, a subset $S$ belongs to $F$ if and only if every <ultrafilter> extending $F$ contains $S$. If $S\notin F$, every $A\in F$ meets $I\setminus S$ in an infinite set; otherwise a cofinite restriction of $A$ would be contained in $S$. Adjoining $I\setminus S$ therefore generates a proper free filter. The <ultrafilter lemma> extends it to a <nonprincipal ultrafilter> witnessing failure of membership.