Reflexivity is equivalent to weak subsequential compactness of bounded sequences

The norm-closed unit ball $B_X$ is weakly closed under HB. Indeed, if $x\mathrm{\notin }{B}_X$, then $\mathrm{\parallel }x\mathrm{\parallel }>1$ and [F3] gives $f\in X^{\ast }$ with $\mathrm{\parallel }f\mathrm{\parallel }=1$ and $f(x)=\mathrm{\parallel }x\mathrm{\parallel }$. The weakly open set $\{y:\mathrm{\mid }f(y)\mathrm{\mid }>1\}$ contains $x$ and misses $B_X$, since $\mathrm{\mid }f(y)\mathrm{\mid }\le \mathrm{\parallel }y\mathrm{\parallel }\le 1$ there. Thus every exterior point has a weak neighborhood in the complement. This also covers $X=\{0\}$, when there is no exterior point.

Suppose $X$ is reflexive and let $(x_n)$ be norm bounded. Fix $R\ge 0$ with $\mathrm{\parallel }{x}_n\mathrm{\parallel }\le R$ for every $n$. If $R=0$, then $x_n=0$ for all $n$ and the identity subsequence converges weakly to zero. Hence it remains to consider $R>0$ and the sequence $y_n=x_n\mathrm{/}R\in B_X$.

Conversely, suppose every norm-bounded sequence in $X$ has a weakly convergent subsequence. Every sequence in $B_X$ is bounded by $1$, so it has a subsequence converging weakly to a point of the ambient space $X$. Thus $B_X$ is relatively weakly sequentially compact.

In the positive-radius case of step 1.2, [F1] makes $B_X$ weakly compact, and step 1.1 makes its weak closure equal to itself, so it is relatively weakly compact. By [F2], some subsequence $y_{n_k}$ converges weakly to $y\in X$. For every $f\in X^{\ast }$, $f(x_{n_k})=Rf(y_{n_k})\to Rf(y)=f(Ry)$, so $x_{n_k}\to Ry$ weakly. Together with the zero-radius case, every bounded sequence has the required subsequence.

Under the hypothesis of step 1.3, [F2] makes $B_X$ relatively weakly compact. Its weak closure is $B_X$ by step 1.1, so $B_X$ itself is weakly compact.

Apply the reverse implication of [F1] to step 2.2. The weak compactness of $B_X$ implies that $X$ is reflexive.

Steps 2.1 and 3.1 prove the two implications, including $X=0$, bound $R=0$, the closed-ball endpoint $\mathrm{\parallel }{x}_n\mathrm{\parallel }=R$, and both scalar fields. The ultrafilter lemma is spent through the compact-unit-ball criterion and Eberlein–Šmulian, DC through Eberlein–Šmulian, and HB through those two suppliers and dual norming; no full Axiom of Choice is used.