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

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.

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.