Theorem: Bipolar Theorem/Absolute Polar

Let $\GF \in \set {\R, \C}$.
Let $\innerprod X {X'}$ be a dual system over $\GF$.
Let $A \subseteq X$ be a non-empty set. 
Let $\paren {A^\circ}_\circ$ be the bipolar of $A$.
Let $\map \sigma {X, X'}$ be the weak topology on $X$ induced by $\innerprod X {X'}$. 
Let $\map {\operatorname {convbal} } A$ be the convex balanced hull.
Let $\cl_\sigma$ denote closure taken in $\map \sigma {X, X'}$.
Then:
:$\paren {A^\circ}_\circ = \map {\cl_\sigma} {\map {\operatorname {convbal} } A}$

Proof:
From Bipolar Set is Convex, $\paren {A^\circ}_\circ$ is convex.
From Bipolar Set is Balanced, $\paren {A^\circ}_\circ$ is balanced.
From Bipolar Set is Closed in Weak Topology, $\paren {A^\circ}_\circ$ is $\map \sigma {E, F}$-closed.
From Bipolar Set contains Original Set, we have $A \subseteq \paren {A^\circ}_\circ$.
Note that we have, from Closure of Convex Balanced Hull as Intersection of Closed Convex Balanced Sets containing Set:
:$\ds \map {\cl_\sigma} {\map {\operatorname {convbal} } A} = \bigcap \set {C \supseteq A : C \text { is convex, balanced and } \map \sigma {X, X'} \text {-closed} }$
From what we have just argued, we have:
:$\paren {A^\circ}_\circ \in \set {C \supseteq A : C \text { is convex, absorbing and } \map \sigma {X, X'} \text {-closed} }$
Hence we have:
:$\map {\cl_\sigma} {\map {\operatorname {convbal} } A} \subseteq \paren {A^\circ}_\circ$
For brevity, write $B = \map {\cl_\sigma} {\map {\operatorname {convbal} } A}$.
{{AimForCont}} that $\paren {A^\circ}_\circ \not \subseteq B$.
Let $a \in \paren {A^\circ}_\circ$ be such that $a \not \in B$.
From Finite Topological Space is Compact, $\set a$ is compact.
Further, from Singleton is Convex Set, $\set a$ is convex.
Applying Hahn-Banach Separation Theorem: Hausdorff Locally Convex Space: Complex Case: Compact Convex Set and Closed Convex Set to $\set a$ and $B$, there exists $\alpha \in \R$ and a $\map \sigma {E, F}$-continuous linear functional $\phi$ such that:
:$\ds \map \Re {\map \phi a} < \alpha < \inf_{x \mathop \in B} \map \Re {\map \phi x}$
Replacing $\phi$ with $-\phi$, we obtain:
:$\ds \sup_{x \mathop \in B} \map \Re {\map \phi x} < -\alpha < \map \Re {\map \phi a}$
From Continuity of Linear Functionals in Weak Topology Induced by Pair of Vector Spaces with Bilinear Mapping, there exists $x' \in X'$ such that:
:$\map \phi x = \innerprod x {x'}$ for each $x \in X$.
Hence we have:
:$\ds \sup_{x \mathop \in B} \map \Re {\innerprod x {x'} } < -\alpha < \map \Re {\innerprod a {x'} }$
That is:
:$\map \Re {\innerprod x {x'} } < -\alpha$ for each $x \in B$.
For each $x \in B$, let $\theta_x \in \R$ be such that $e^{i \theta_x} \innerprod x {x'} = \cmod {\innerprod x {x'} }$. 
Since $B$ is balanced, we have $e^{i \theta_x} x \in B$.
Hence we have:
:$\map \Re {\innerprod {e^{i \theta_x} x} {x'} } = \map \Re {e^{i \theta_x} \innerprod x {x'} } = \cmod {\innerprod x {x'} } < -\alpha$
Hence $\beta = -\alpha > 0$.
Let:
:$\ds y' = \frac {x'} \alpha$
Then we have:
:$\cmod {\innerprod x {y'} } < 1$ for all $x \in B$
and:
:$\map \Re {\innerprod a {y'} } > 1$
by bilinearity.
Then:
:$\cmod {\innerprod a {y'} } > 1$
Since $A \subseteq B$, as the intersection of sets containing $A$, we then have:
:$\cmod {\innerprod x {y'} } < 1$ for all $x \in A$
Hence we have $y' \in A^\circ$. 
However, since $\cmod {\innerprod a {y'} } > 1$, we have that $\cmod {\innerprod a {y'} } \le 1$ fails for some $y' \in A^\circ$.
Hence $a \not \in \paren {A^\circ}_\circ$.
This is a contradiction to our assumption that $a \in \paren {A^\circ}_\circ$. 
Hence $B = \paren {A^\circ}_\circ$.
{{qed}}