Closed subspaces of reflexive spaces are reflexive

Let $R:X^{\ast }\to Y^{\ast }$ be restriction, $R(f)=f{\mathrm{\mid }}_Y$. It is scalar-linear and bounded with $\parallel Rf\parallel \le \parallel f\parallel$. Hence for a supplied $y^{\ast \ast }\in Y^{\ast \ast }$ the composite $x^{\ast \ast }=y^{\ast \ast }\circ R$ belongs to $X^{\ast \ast }$. Since $X$ is reflexive, [F1] supplies $x\in X$ such that $J_{X}x=x^{\ast \ast }$, meaning $f(x)=y^{\ast \ast }(f{\mathrm{\mid }}_Y)$ for every $f\in X^{\ast }$.

If $f\in Y^{\perp }$, then $f{\mathrm{\mid }}_Y=0$, so step 1.1 gives $f(x)=y^{\ast \ast }(0)=0$. Thus every functional annihilating $Y$ also annihilates $x$.

We claim $x\in Y$. This is immediate if $Y=X$. Otherwise suppose $x\mathrm{\notin }Y$; then $Y$ is a nonempty closed convex set and [F3] supplies $0\mathrm{\ne }f\in X^{\ast }$, $a\in \mathbb{R}$, and $\epsilon >0$ with $\mathrm{Re}f(y)\le a-\epsilon <a+\epsilon \le \mathrm{Re}f(x)$ for every $y\in Y$. Since $ty\in Y$ for every real $t$, the real-linear function $\mathrm{Re}f$ can be bounded above on the line $\mathbb{R}y$ only when $\mathrm{Re}f(y)=0$. In the complex case applying this also to $iy\in Y$ gives $\mathrm{Re}f(iy)=-\mathrm{Im}f(y)=0$, so in either field $f{\mathrm{\mid }}_Y=0$. Taking $y=0$ in the separation inequality gives $0\le a-\epsilon$ and hence $\mathrm{Re}f(x)\ge a+\epsilon \ge 2\epsilon >0$, contradicting step 2.1. Therefore $x\in Y$.

Let $g\in Y^{\ast }$ be arbitrary. By norm-preserving Hahn–Banach [F6], one functional $f\in X^{\ast }$ extends $g$; this also covers $g=0$ and $Y=\{0\}$. Steps 1.1 and 3.1 then give $y^{\ast \ast }(g)=y^{\ast \ast }(f{\mathrm{\mid }}_Y)=f(x)=g(x)=(J_{Y}x)(g)$. Hence $y^{\ast \ast }=J_{Y}x$.

The closed-subspace theorem [F4] makes $Y$ a Banach space. Since the arbitrary $y^{\ast \ast }\in Y^{\ast \ast }$ of step 1.1 lies in the range of $J_Y$ by step 4.1, that canonical map is surjective, and [F1] makes $Y$ reflexive. If $Y=0$, its bidual and all maps above are zero and the same argument gives the singleton range directly.

HB is used exactly twice: geometric separation in step 3.1 and the extension of one supplied $g$ in step 4.1; [F5] records the principle being assumed. No compactness principle or simultaneous family choice occurs.