Proposition 5

Let F, F' be two subspaces of a vector space E, such that $F \subset F'$. Then $\operatorname{codim}_E F' \leq \operatorname{codim}_E F \leq \dim E$. If $\operatorname{codim}_E F$ is finite, the relation $\operatorname{codim}_E F' = \operatorname{codim}_E F$ implies $F = F'$.

The inequality $\operatorname{codim}_E F \leq \dim E$ is obvious from (9) and if $\dim E$ is finite the relation $\operatorname{codim}_E F = \dim E$ implies $\dim F = 0$ and hence $F = \{0\}$. The remainder of the proposition follows from this, for

since $E/F'$ is canonically isomorphic to $(E/F)/(F'/F)$ (I, § 4, no. 7, Theorem 4).