Let $E$ be a $k$-vector space. Remember that for any subset $A\subset E$, the orthogonal of $A$ is defined as
$$A^{\perp}:=\{\lambda\in E^* | \forall x\in A, \lambda(x)=0\}$$
Now, let $F$ and $G$ be two subspaces of $E$. Of course, we have the implication $$F\subset G \implies G^{\perp}\subset F^{\perp}$$ but I am interested in the converse. Every reference I have only states the above implication without giving a word about the converse. I think I am able to show it, however I now have a doubt about the validity of my proof. Could someone please validate or tell me where I am wrong (aside from the fact that I am using the axiom of choice) ?
Thank you very much !
$$G^{\perp}\subset F^{\perp} \implies F\subset G$$
Proof: Suppose $G^{\perp}\subset F^{\perp}$ and assume toward a contradiction that there exists some $x\in F\setminus G$. Consider a basis $\mathcal B$ of $G$. Then, the family $\mathcal B \cup \{x\}$ is still free, as $x$ does not lie in $G$. Hence, we may complete $\mathcal B \cup \{x\}$ into a basis $\{e_i\}_{i\in I}$ of $E$. Let us then rewrite $x=e_{i_0}$ and $\mathcal B = \{e_j\}_{j\in J}$ for some $i_0\in I$ and $J\subset I$. Naturally, $i_0\not \in J$.
Now that we have a basis, we may consider the dual family $\{e_i^*\}_{i\in I}$ in $E^*$ defined by the formulae $e_i^*(e_j)=\delta_{i,j}$.
Because $e_{i_0}^*(x)=1$, we see that $e_{i_0}^*\not \in F^{\perp}$. However, for every $j\in J$, we do have $e_{i_0}^*(e_j)=0$. As the family $\{e_j\}_{j\in J}$ is a basis of $G$, we see that $e_{i_0}^* \in G^{\perp}$.
This is absurd, and concludes the proof.