Double orthogonal complement of a finite dimensional subspace w.r.t. a nondegenerate symmetric bilinear form on an infinite dimensional space 
Let $U$ be a finite-dimensional subspace of an infinite-dimensional space $V$ equipped with a nondegenerate symmetric bilinear form $\phi$. Is it necessarily true that ${(U^{\perp})}^{\perp}=U$?

If the bilinear form happens to be an inner product, then the statement is true (see here). If $V$ is finite dimensional, the statement follows from dimension count. I believe the statement as formulated is false. Anyone knows a counterexample? What if I impose the extra condition that the restriction of $\phi$ to $U$ is nondegenerate?
 A: Yes, it is necessarily true
First, note that $U \subseteq U^{\perp\perp}$ will always hold, regardless of degeneracy. Indeed: by the definition of $U^{\perp}$, $(x,y) = 0$ holds for all $x \in U$ and $y \in U^\perp$. Thus, if $x \in U$, then $(x,y) = 0$ holds for all $y \in U^\perp$. Thus, $x$ is an element of $(U^\perp)^\perp$.
The more complicated part is showing that $U^{\perp\perp} \subseteq U$.
Let $d = \dim(U)$. Let $\{x_1,\dots,x_d\}$ be a basis of $U$. Consider the map $\phi:V \to \Bbb F^d$ given by
$$
\phi(v) = [(x_1,v),\dots,(x_d,v)].
$$
Notably, $\ker(\phi) = U^\perp$. $\phi$ is a surjective (onto) map. Indeed, suppose for the purpose of contradiction that $\phi$ fails to be surjective. It would follow that there exists there exists a non-zero vector $c = (c_1,\dots,c_d)$ in $\operatorname{im}(\phi)^\perp$, where the orthogonal complement is taken relative to the "dot-product" over $\Bbb F^d$ (i.e. $c,d \mapsto c^Td$). For this $c$, it holds that for all $v \in V$,
$$
c^T\phi(v) = 0 \implies\\
c_1(x_1,v) + \cdots + c_d(x_d,v) = 0 \implies\\
(c_1 x_1 + \cdots + c_d x_d,v) = 0.
$$
By the non-degeneracy of the bilinear form, this implies that $c_1 x_1 + \cdots + c_d x_d = 0$. Because $\{x_1,\dots,x_d\}$ is a basis, this implies that $c = 0$, contradicting our statement that $c$ is non-zero.
This allows us to deduce that the quotient space $V/\ker(\phi) = V/U^{\perp}$ has dimension $d$, and that $\phi$ induces an isomorphism $\bar \phi:(V/U^\perp) \to \Bbb F^d$ via the quotient map.
Now, suppose that $x \in U^{\perp\perp}$. Consider the linear map $\alpha:V \to \Bbb F$ given by $\alpha(v) = (x,v)$. Because $U^\perp \subseteq \ker(\alpha)$, $\alpha$ induces a linear map $\bar \alpha:(V/U^\perp) \to \Bbb F$. Because $\bar \phi$ is an isomorphism, there exists a vector $c = (c_1,\dots,c_d) \in \Bbb F^d$ such that $\bar \alpha(v + U^\perp) = c^T\bar\phi(v + U^\perp)$. Correspondingly, we may conclude that for all $v \in V$, we have
$$
\alpha(v) = c^T\phi(v) \implies (x,v) = (c_1x_1 + \cdots + c_dx_d,v) \implies\\
(c_1 x_1 + \cdots + c_d x_d - x,v) = 0 \quad \text{for all } v \in V.
$$
Because the bilinear form is non-degenerate, we may conclude that $c_1 x_1 + \cdots + c_d x_d - x = 0$, which is to say that $x = c_1x_1 + \cdots + c_dx_d$, which means that $x \in U$.
Thus, we have $U^{\perp \perp} \subseteq U$. Thus, we have shown that $U = U^{\perp\perp}$.
