A more direct proof of Goldstine theorem I'm trying to give a more direct proof of Goldstine theorem. Could you have a check on my attempt?

Let $E$ be a normed space, $E'$ its dual, and $E''$ its bidual. Let $B_E$ and $B_{E''}$ be the closed unit balls of $E$ and $E''$ respectively. Let $\sigma(E'', E')$ be the weak$^\star$ topology on $E''$. Let $J:E \to E'', x \mapsto \hat x$ be the canonical injection. Then $J[B_E]$ is dense in $B_{E''}$ w.r.t. $\sigma(E'', E')$.

I posted my proof separately so that I can accept my own answer to remove my question from unanswered list. Surely, if other people post answers, then I will happily accept theirs.
 A: Let $\overline{J[B_E]}$ be the closure of $J[B_E]$ in the subspace topology that $\sigma(E'', E')$ induces on $B_{E''}$. By Banach–Alaoglu theorem, $B_{E''}$ is compact. Compact sets are closed in Hausdorff topology, so $B_{E''}$ is closed in $\sigma(E'', E')$. It follows that $\overline{J[B_E]}$ is the closure of $J[B_E]$ in $\sigma(E'', E')$.
Assume the contrary that $\overline{J[B_E]} \subsetneq B_{E''}$. Then there is $\varphi \in B_{E''} \setminus \overline{J[B_E]}$. Singletons are compact in Hausdorff topology, so $\{\varphi\}$ is compact in $\sigma(E'', E')$. Clearly, $\{\varphi\}$ and $B_{E''}$ are non-empty convex. Notice that $E''$ together with $\sigma(E'', E')$ is a locally convex t.v.s., so we can apply Hahn–Banach theorem to strictly separate $\{\varphi\}$ and $\overline{J[B_E]}$.
This means there exist $s, t \in \mathbb R$ and a linear map $\Psi:E'' \to \mathbb R$ that is continuous in $\sigma(E'', E')$ such that
$$
\langle \Psi , \psi \rangle < s <t < \langle \Psi, \varphi  \rangle, \quad \forall \psi \in \overline{J[B_E]}.
$$

Lemma: Let $\varphi: E' \rightarrow \mathbb{R}$ be a linear functional that is continuous for the weak$^{\star}$ topology. Then there exists some $x \in E$ such that
$$
\langle \varphi, f \rangle = \left\langle f, x \right\rangle, \quad \forall f \in E' .
$$

By our Lemma, there is $f \in E'$ such that $\langle \Psi, \psi \rangle = \langle \psi, f \rangle$ for all $\psi \in E''$. Then
$$
\langle \psi, f \rangle < s <t< \langle \varphi , f \rangle, \quad \forall \psi \in \overline{J[B_E]}.
$$
First, $t < \langle \varphi , f \rangle\le \|\varphi\| \cdot \|f\| \le\|f\|$ because $\varphi \in B_{E''}$. Second, $\langle \psi, f \rangle < s$ for all $\psi \in \overline{J[B_E]}$ implies $\langle Jx, f \rangle = \langle f, x \rangle< s$ for all $x\in B_E$. This in turn implies $\|f\| \le s$. Hence we obtain a contradiction $$\|f\| \le s<t \le \|f\|.$$
This completes the proof.
