Stone clopen representation under BPI

If $b\le ̸c$, the element $d=b\wedge \mathrm{\neg }c$ is nonzero, and $\{a:d\le a\}$ is a proper filter. F2 extends it to $U$ with $b\in U$ and $c\mathrm{\notin }U$, since otherwise $d\wedge c=0$ would belong to $U$. Thus $[b]\subseteq ̸[c]$. Together with the Boolean identities in F1, this shows that $b\mapsto [b]$ is an injective Boolean homomorphism, reflecting order.

If $U,V$ are distinct ultrafilters, some $b$ belongs to exactly one; the other contains $\mathrm{\neg }b$. The disjoint open sets $[b]$ and $[\mathrm{\neg }b]$ separate them, so $X$ is Hausdorff.

Consider a cover $\{[b]:b\in H\}$ with no finite subcover. No finite join from $H$ is $1$, since F1 would make those finitely many clopens cover $X$. Hence every finite meet from $\{\mathrm{\neg }b:b\in H\}$ is nonzero, including the empty meet (otherwise $B$ is trivial and the empty subcover suffices). Their upward closure is a proper filter: concatenation of finite lists gives meet closure, and no witness meet is zero. F2 extends it to an ultrafilter $U$. For every $b\in H$, $\mathrm{\neg }b\in U$ forces $U\mathrm{\notin }[b]$, contradicting the cover. Thus every basic cover has a finite subcover.

Given an arbitrary open cover $\mathcal{O}$, let $H$ consist of all $b$ such that $[b]\subseteq O$ for some $O\in \mathcal{O}$. The basis property in F1 makes these sets a cover; step 1.3 gives finitely many covering basic sets. For each of this finite list take one containing member of $\mathcal{O}$. These form a finite subcover, proving compactness with only finite choice.

For a clopen $K\subseteq X$, all basic clopens contained in $K$, together with the open set $X\setminus K$, cover $X$. Step 2.1 supplies a finite subcover; intersecting its union with $K$ gives $K=[b_1]\cup \cdots \cup [b_n]=[b_1\vee \cdots \vee b_n]$. If the finite list is empty, $K=\mathrm{\varnothing }=[0]$. Hence the embedding in step 1.1 is onto all clopens. If $B$ is trivial, $X=\mathrm{\varnothing }$ and both algebras have one element; the same identities and compactness conclusion hold. QED.