Annihilators are weak and weak star closed

By F1, $M^{\perp }$ is the intersection over $m\in M$ of the kernels of $f\mapsto f(m)$, and ${}^{\perp }N$ is the intersection over $f\in N$ of $\ker f$. Each kernel is a linear subspace and closed in the corresponding topology by F2 and closedness of $\{0\}\subseteq \mathbb{K}$. Intersections preserve both properties; empty intersections give the whole ambient spaces.

For linear $N$, F3 yields $({}^{\perp }N{)}^{\perp }={\bar{N}}^{w^{\ast }}$ with no primal norming used. For linear $M$, every functional vanishing on $M$ also vanishes on its norm closure, by norm continuity. Thus ${\bar{M}}^{\mathrm{\parallel }\cdot \mathrm{\parallel }}\subseteq {}^{\perp }(M^{\perp })$. Step 1.1 also implies ${\bar{M}}^w\subseteq {}^{\perp }(M^{\perp })$.

Assume HB and fix $x\mathrm{\notin }K={\bar{M}}^{\mathrm{\parallel }\cdot \mathrm{\parallel }}$. The set $K$ is a nonempty closed linear subspace: addition and scalar multiplication preserve closure by their norm estimates. By F4 there is $f\in X^{\ast }$ whose real part is bounded above on $K$ and strictly larger at $x$. Since $K$ is a real linear subspace, scaling forces $\mathrm{Re}f=0$ on $K$. In the complex case $ik\in K$ forces $\mathrm{Im}f(k)=0$ too. Hence $f\in M^{\perp }$ and $f(x)\mathrm{\ne }0$, excluding $x$ from ${}^{\perp }(M^{\perp })$. The open set $\{y:\mathrm{\mid }f(y)\mathrm{\mid }>\mathrm{\mid }f(x)\mathrm{\mid }\mathrm{/}2\}$ also excludes $x$ from ${\bar{M}}^w$. Norm closure is contained in weak closure because weak-open sets are norm open; all three sets therefore coincide. $\mathrm{\square }$