Boolean ultrafilter extension

The poset $\mathcal{P}$ of proper filters of $B$ containing $F$, ordered by inclusion, is nonempty because $F\in \mathcal{P}$. Every nonempty chain $\{F_i\}$ in $\mathcal{P}$ has an upper bound: the union $G:={\bigcup }_i{F}_i$ is a filter (it contains $1$; it omits $0$ since $0$ in the union would put $0$ in some $F_i$; it is closed under $\wedge$ because two elements lie in a common $F_i$ by directedness of a chain, and it is upward closed because each $F_i$ is), and $G$ contains $F$.

By [L2], applied under the standing Axiom of Choice, $\mathcal{P}$ has a maximal element $U$, a proper filter containing $F$ that is maximal among proper filters, hence an ultrafilter by [L1]; this proves claim 1.

If $U$ is an ultrafilter and $a\mathrm{\notin }U$, the filter generated by $U\cup \{a\}$ cannot be proper, by maximality in [L1]. Hence some $u\in U$ satisfies $u\wedge a=0$: otherwise the family of elements above some $u\wedge a$ would be a proper filter strictly containing $U$. Thus $u\le \mathrm{\neg }a$, so $\mathrm{\neg }a\in U$ by upward closure. Conversely $a$ and $\mathrm{\neg }a$ cannot both lie in a proper filter because their meet is $0$. Therefore exactly one of $a\in U$, $\mathrm{\neg }a\in U$ holds.

For $a\mathrm{\ne }b$ the symmetric difference $c:=a\mathrm{△}b$ has $c\mathrm{\ne }0$ by [L3], so the principal filter $F_c:=\{d:d\ge c\}$ is proper ($0\ge ̸c$); by [step 1.2] it is contained in an ultrafilter $\mathcal{U}$, which therefore contains $c$.

If $a\in \mathcal{U}$ then $c\wedge a=a\wedge \mathrm{\neg }b\in \mathcal{U}$, while $b\mathrm{\notin }\mathcal{U}$, since $b\in \mathcal{U}$ would give $a\wedge b\in \mathcal{U}$ and then $0=c\wedge a\wedge b\in \mathcal{U}$; symmetrically, if $a\mathrm{\notin }\mathcal{U}$ then by [step 1.3] $\mathrm{\neg }a\in \mathcal{U}$ and the same computation with the roles exchanged gives $b\in \mathcal{U}$. Hence $\mathcal{U}$ contains exactly one of $a,b$, proving claim 2.