Let $V$ be a vector space having a basis consisting of $n$ elements. Let $W$ be a subspace which does not consist of $O$ alone. Then $W$ has a basis, and the dimension of $W$ is $\leq n$.
#### Proof
Let $W \ni w_{1}\neq0$
If $\left\{w_{1}\right\}$ is not a [[maximal subset of independent vectors|maximal]] of $W$, $\exists w_{2}\in W$ such that $w_{1}, w_{2}$ are linearly independent.
If $\left\{w_1,\ldots,w_{i}\right\}$ is not a [[maximal subset of independent vectors|maximal]] of $W$, $\exists w_{i+1}\in W$ such that $w_{1}, \ldots w_{i+1}$ are linearly independent.
Inductively reason $\mathbb{Z}\ni m \leq n$ such that we can find linearly independent elements $w_{1}, w_{2}, \ldots, w_{m}$, and such that
$
\left\{w_{1}, \ldots, w_{m}\right\}
$
is a maxmal set of linearly independent elements of $W$ knowing we will stop eventually because [[larger sets of vectors than the maximal are dependent]], so $m$ cannot exceed $n$.
[[maximal subsets form a basis]]