A Stone space is recovered from its clopens

For $x\in X$, the clopens containing $x$ include $X$, exclude $\mathrm{\varnothing }$, are upward and intersection closed, and decide each pair $C,X\setminus C$. By F2 this is an ultrafilter, so ${\eta }_X$ is defined. If $x\mathrm{\ne }y$, Hausdorffness gives an open neighborhood of $x$ avoiding $y$, and the clopen basis gives a clopen $C$ containing $x$ but not $y$. Thus ${\eta }_X(x)\mathrm{\ne }{\eta }_X(y)$.

Let $U$ be an ultrafilter of clopens. Its finite intersections are members of $U$ and are nonempty, so its closed sets have FIP, including the empty intersection $X$. F3 supplies $x\in \bigcap U$. If a clopen $C$ containing $x$ were absent from $U$, F2 would put $X\setminus C$ in $U$, contrary to the choice of $x$. Hence $U={\eta }_X(x)$. This point is unique by step 1.1.

For each clopen $C$, the definitions give ${\eta }_X^{-1}([C])=C$. Thus ${\eta }_X$ is continuous on the basic opens, hence on their unions. Surjectivity in step 2.1 gives ${\eta }_X[C]=[C]$ as well. Every open set of $X$ is a union of clopens, so its image is a union of basic open sets; the inverse of the bijection is continuous. If $X=\mathrm{\varnothing }$, its clopen algebra is trivial, its ultrafilter space is empty, and the empty map is the asserted homeomorphism. The inverse is defined by the unique common point, without choice. QED.