The basis theorem for vector spaces states that every vector space admits a basis, or in other words is a free module over its ground field of scalars. It is a famous classical consequence of the axiom of choice (and is equivalent to it by a result of Andreas Blass, proved in 1984).
is an upper bound, for each in the span of belongs to some and is uniquely expressible as a finite linear combination of elements in and in any containing , hence uniquely expressible as a finite linear combination of elements in . Thus the hypothesis of Zorn’s lemma obtains for this poset; therefore this poset has a maximal element, say .
Let be the span of . If were a proper subspace of , then for any in the set-theoretic complement of , is a linearly independent set (for if
we must have – else we can multiply by and express as a linear combination of the , contradicting – and then the remaining are 0 since the are linearly independent). This contradicts the maximality of . We therefore conclude that , and is a basis for .
I’ll write out a proof of the converse, that the axiom of choice follows from the basis theorem, as soon as I’ve digested it – Todd.
Given any linearly independent set and spanning set , if , then there is a basis with ; the theorem above is the special case where and . The proof of this more general theorem is a straightforward generalisation of the proof above.