Finite Boolean algebras are powersets of their atoms

For $b\mathrm{\ne }0$, the finite nonempty set $\{c:0<c\le b\}$ has a minimal member: a strict descending sequence cannot have more distinct terms than this finite set. Such a minimal member is an atom. If atoms $a,d$ have nonzero meet, minimality gives $a\wedge d=a=d$. Thus distinct atoms are disjoint.

Put $s=\bigvee \{a\in A:a\le b\}$. This finite join is at most $b$. If $b\wedge \mathrm{\neg }s\mathrm{\ne }0$, step 1.1 gives an atom $d\le b\wedge \mathrm{\neg }s$. Then $d\le b$ puts $d\le s$, contradicting $d\le \mathrm{\neg }s$ and $d\mathrm{\ne }0$. Hence $b=s$.

Write $\varphi (b)=\{a\in A:a\le b\}$. Meets correspond to intersections by the definition of lower bound. For an atom $a$, the equation $a=(a\wedge b)\vee (a\wedge \mathrm{\neg }b)$ implies exactly one of $a\le b$ and $a\le \mathrm{\neg }b$, since each piece is $0$ or $a$. Therefore complements correspond to set complements, and joins correspond to unions by De Morgan's law; bounds correspond to $\mathrm{\varnothing },A$. Step 2.1 proves injectivity. For $T\subseteq A$, distinct-atom disjointness gives $\varphi (\bigvee T)=T$: an atom outside $T$ meets that finite join in $0$. This proves surjectivity. If $B$ is trivial, $A=\mathrm{\varnothing }$ and both algebras have one element.

For an ultrafilter $U$, finiteness makes $a=\bigwedge U$ a member of $U$, so $a\mathrm{\ne }0$ and $U=\{b:a\le b\}$. If $0<c<a$, then $c\mathrm{\notin }U$, so F2 gives $\mathrm{\neg }c\in U$ and $a\le \mathrm{\neg }c$, contradicting $0<c\le a$. Hence $a$ is an atom. Conversely the upward filter generated by an atom is proper and decides every pair by step 3.1, so F2 makes it an ultrafilter. Two atoms generating the same filter each lie above the other and are equal. QED.