For any subspace $V$ of a finite dimensional inner product vector space, prove that $(V ^ \perp)^\perp = V$.
My proof is below. I request verification, critique, or improvement.
Note: Other proofs are available. This question is to verify or critique this proof.
Lemma 1: For any vector space $V$, $\dim V = \operatorname{codim} V^\perp$.
Proof: Let $\{v_n\}$ be a basis for $V$, and $[V]^\top$ be the matrix where $\operatorname{row} i = v_i$. Clearly $\operatorname{rank} [V]^\top = \dim V $. The nullspace of $[V]^\top$ is precisely $V^\perp$, since any vector $x$ is both in the nullspace of $[V]^\top$ and in $V^\perp$ if and only if $x$ is orthogonal to each $v_i$. Thus, $\operatorname{codim} V^\perp = \operatorname{codim nullspace} [V]^\top = \operatorname{rank} [V]^\top = \dim V$.
Lemma 2: For any vector spaces $V, W$, if $V \subset W$ and $\dim V = \dim W$, then $V = W$.
Proof: Any basis of $V$ must be a subset of $W$ and therefore a basis of $W$, implying that $V = W$.
Main Proof: By applying Lemma 1 twice, we have $\dim (V ^ \perp)^\perp = \dim V$. Furthermore, since, by definition, any $v \in V$ is in $(V ^ \perp)^\perp$, we have $V \subset (V ^ \perp)^\perp$. Since the perp of a vector space is itself a vector space, we can apply Lemma 2, and have $V = (V ^ \perp)^\perp$.
Remarks: This proof assumes that vector spaces have a finite dimension. I do not know how to determine if it holds for infinite dimensional vector spaces.
Is the proof above correct, rigorous, and well written? How could it be improved?
Update
As recommended by the comments, I've added that $V$ is a subspace of a finite dimensional inner product vector space. With that stipulation, is the proof correct, rigorous, and well written? How could it be improved?