Any nonempty irreflexive Banach space contains a separable irreflexive Banach subspace - is my proof correct?

Question

It is asserted in a proof I am following that:

Let $X$ be a nonempty, irreflexive Banach space. By the Eberlein-Smulian theorem, $X$ contains a subspace $S$ that is Banach, irreflexive and separable.

It gives no further context, so I assume "separable" is in the sense of the strong normed topology.

All I know about the Eberlein-Smulian theorem is that it shows us a nonempty Banach space is reflexive if and only if its closed unit ball is weakly compact, if and only if its closed unit ball is weakly sequentially compact.

Then $X$ nonempty, irreflexive and Banach implies there exists a sequence $(x_n)_{n\in\Bbb N}$ where $\|x_n\|\le1$ for all $n$ and $(x_n)$ possesses no weak sublimit. I know that $S:=\overline{\operatorname{span}\{x_n:n\in\Bbb N\}}$ is a separable Banach subspace, but I am not sure if the following is a correct way to show irreflexivity.

If $S$ were reflexive, then the closed unit ball of $S$ would be weakly compact by Kakutani's theorem, and it would also be weakly sequentially compact by Eberlein-Smulian. Then $(x_n)_{n\in\Bbb N}$, considered as a sequence in the closed unit ball of $S$, would possess a weak sublimit in the weak topology on $S$, but this would imply it possessed a weak sublimit in the weak topology on $X$, a contradiction.

Is this right? It feels a bit trivial, as if I'm missing some detail.

Answer 1

If $y_i \to y$ weakly in $S$ then $y_i \to y$ weakly in $X$ also: any continuous linear functional on $X$ leads to a continuous linear functional on $S$ by restriction. Hence, above argument is correct.