Eberlein–Šmulian separable reduction

Let ${\mathbb{Q}}_{\mathbb{K}}=\mathbb{Q}$ in the real case and $\mathbb{Q}+i\mathbb{Q}$ in the complex case, with the canonical embeddings into the scalar field understood. By [F2], ${\mathbb{Q}}_{\mathbb{K}}$ is at most countable: in the complex case it is the image of the countable product $\mathbb{Q}\times \mathbb{Q}$. It is nonempty, so fix one surjection $q:\mathbb{N}\to {\mathbb{Q}}_{\mathbb{K}}$. This is one instantiation of the countability theorem, not a countable family of choices.

The scalar set ${\mathbb{Q}}_{\mathbb{K}}$ is dense in $\mathbb{K}$. This is [F3] over $\mathbb{R}$. Over $\mathbb{C}$, approximate the real and imaginary parts separately and use $\mathrm{\mid }(a+ib)-(r+is)\mathrm{\mid }\le \mathrm{\mid }a-r\mathrm{\mid }+\mathrm{\mid }b-s\mathrm{\mid }$.

Every $F\in X^{\ast }$ restricts to a member of $Y^{\ast }$, so every ambient weak subbasic set has an intrinsically weak-open trace on $Y$. Conversely, given one $g\in Y^{\ast }$, [F4] supplies $F\in X^{\ast }$ with $F{\mathrm{\mid }}_Y=g$. Therefore the inverse image under $g$ of any scalar-open set is the trace on $Y$ of the corresponding ambient weak-open inverse image under $F$. Finite intersections behave the same way. The two topologies on $Y$ are equal.

The set ${\mathbb{N}}^{<\mathbb{N}}$ of finite strings of naturals has a choice-free enumeration: order strings first by $\mathrm{\mid }s\mathrm{\mid }+{\sum }_{j<\mathrm{\mid }s\mathrm{\mid }}s(j)$, then by length, and then lexicographically. Each fixed-value block is finite, and the displayed order lists every finite string. Map $s=(s(0),\dots ,s(m-1))$ to $d_s={\sum }_{j=0}^{m-1}q(s(j))x_j$, with empty sum $0$. Its image $D=\{d_s:s\in {\mathbb{N}}^{<\mathbb{N}}\}$ is nonempty and at most countable by [F2].

The set $D$ is norm dense in ${\mathrm{span}}_{\mathbb{K}}\{x_n:n\in \mathbb{N}\}$. Indeed, write a given vector there as $u={\sum }_{j=0}^{m-1}{\alpha }_j{x}_j$, padding with zero coefficients when necessary. If $m=0$, then $u=0=d_{\mathrm{\varnothing }}$. If $m>0$ and $\epsilon >0$, put $S={\sum }_{j<m}(1+\mathrm{\parallel }{x}_j\mathrm{\parallel })>0$. By step 1.2, make the finitely many choices $r_j\in {\mathbb{Q}}_{\mathbb{K}}$ with $\mathrm{\mid }{\alpha }_j-r_j\mathrm{\mid }<\epsilon \mathrm{/}S$. Choose indices $k_j$ with $q(k_j)=r_j$; only finitely many choices are involved. For $s=(k_0,\dots ,k_{m-1})$, the triangle inequality gives $\mathrm{\parallel }u-d_s\mathrm{\parallel }\le {\sum }_{j<m}\mathrm{\mid }{\alpha }_j-r_j\mathrm{\mid }\mathrm{\parallel }{x}_j\mathrm{\parallel }<(\epsilon \mathrm{/}S){\sum }_{j<m}\mathrm{\parallel }{x}_j\mathrm{\parallel }<\epsilon$. Thus ${\bar{D}}^{\mathrm{\parallel }\cdot \mathrm{\parallel }}=Y$.

By [F1] and step 3.1, $Y$ is separable. The norm closure of a linear subspace is again linear: approximating two vectors and using the triangle inequality proves closure under addition, and multiplying an approximating net by one fixed scalar proves closure under scalar multiplication, including the scalar zero. Hence $Y$ is a closed linear subspace of the Banach space $X$, so [F6] makes $Y$ Banach.

Finally take $z\in X\setminus Y$. The set $Y$ is nonempty, closed and convex, while $\{z\}$ is compact and disjoint from it. By [F5], there are $f\in X^{\ast }$, $a\in \mathbb{R}$ and $\delta >0$ such that $\mathrm{Re}f(y)\le a-\delta <a+\delta \le \mathrm{Re}f(z)$ for every $y\in Y$. The weakly open set $\{w\in X:\mathrm{Re}f(w)>a\}$ contains $z$ and misses $Y$. Every point of $X\setminus Y$ therefore has a weak neighborhood in the complement, so $Y$ is weakly closed. This uses HB only through [F4] and [F5]: the proof never selects extensions or separators simultaneously for a family.