Ultrafilter lemma (source code)

= Ultrafilter lemma
{wiki}

Every proper <filter on a set> is contained in an <ultrafilter>. Order its proper filter extensions by inclusion, use <Zorn lemma> to obtain a maximal extension, and observe that maximality forces it to contain exactly one of every set and its complement.