Theorem

Every finite-dimensional vector space has a basis.

Proof

By definition, finite dimensional vector spaces have a spanning list. 2.30 dictates that every spanning list can be reduced to a basis by throwing out some unnecessary vectors. Thus, this is proven.