Theorem 2

For every orthonormal set L in a hilbertian space E, there exists an orthonormal basis B of E containing L.

In fact, let $\mathfrak{D}$ be the family of all orthonormal subsets of E, linearly ordered by inclusion; it is immediate that this family has finite character (S, III, § 4, No. 5). Hence there exists a maximal family B in $\mathfrak{D}$ containing L, by th. 1 of S, III, § 4, No. 5. It remains to prove that B is a total set. If not, there will exist a vector $y \neq 0$ which is orthogonal to all the vectors of B (V, p. 22, prop. 5), and multiplying y by a suitable scalar, we can assume that $\|y\| = 1$; then, $B \cup \{y\}$ will be an orthonormal set distinct from B and containing B; this contradicts the definition of B; hence the theorem.