Corollary 1

Suppose that $A$ is a field and that $\Phi$ is non-degenerate. For a subspace $M$ of $E$ to be of finite dimension, it is necessary and sufficient that $M^0$ be of finite codimension in $F$, and one then has $\operatorname{codim} M^0 = \dim M$, and $M^{00} = M$.

Comme $F^0 = \{0\}$, the first two assertions result from prop. 4 applied to the restriction of $\Phi$ to $M \times F$. Moreover, $M^0$ is the orthogonal of $M^{00}$, hence $M^{00}$ is of finite dimension equal to $\operatorname{codim} M^0 = \dim M$; but since $M^{00} \supset M$, we have $M^{00} = M$.