Zorn's lemma gives a basis between any linearly independent set and any spanning set containing it: if $L\subseteq S\subseteq V$ with $L$ independent and $\mathrm{span}(S)=V$, there is a basis $B$ of $V$ with $L\subseteq B\subseteq S$

Assume the Axiom of Choice (The Axiom of Choice), which is what Zorn's lemma is proved from. Let $V$ be a vector space over a field $F$ (Vector space over a field) and let $L\subseteq S\subseteq V$ with $L$ linearly independent (Linear independence: a finite list $v:n\to V$ is independent when ${\sum }_{i<n}{\lambda }_i{v}_i=0_V$ forces every ${\lambda }_i=0_F$, and a subset $S\subseteq V$ is independent when every injective finite list into $S$ is independent) and $\mathrm{span}(S)=V$ (Linear combination of a finite list, and the span $\mathrm{span}(S)$ as the smallest linear subspace containing $S$). Then there is a basis $B$ of $V$ (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis) with

$L\subseteq B\subseteq S\mathrm{.}$

• Both classical statements are instances of this one. "Every vector space has a basis" is the case $L=\mathrm{\varnothing }$, $S=V$ (Every vector space has a basis), and "every spanning set contains a basis" is the case $L=\mathrm{\varnothing }$ (Every spanning subset of a vector space contains a basis). They are corollaries of this single Zorn argument rather than two separate ones, which is why the two hypotheses are stated together in the statement above.

• The choice is declared, not hidden. The only non-constructive ingredient is Zorn's lemma, and that item records that the Axiom of Choice is used exactly once inside it. Nothing else above appeals to a choice principle: the poset, its order and the upper bound of a chain are all written down explicitly. Zorn's lemma is equivalent to the Axiom of Choice over ZF (The Axiom of Choice and Zorn's lemma are equivalent), so the cost of this theorem is exactly that axiom.

• The empty chain is a real case here. Zorn's lemma as proved in this library has no nonemptiness clause on chains, and its own remarks note that requiring every chain to have an upper bound already forces the poset to be nonempty. In the poset above the union of the empty chain is $\mathrm{\varnothing }$, which lies in $P$ only when $L=\mathrm{\varnothing }$; the upper bound supplied instead is $L$. Skipping this case would leave a hole in the verification of Zorn's hypothesis.

• Maximality is used exactly once, in step 3.1, and only to exclude one extra vector at a time. That is why If $S\subseteq V$ is linearly independent and $w\mathrm{\notin }\mathrm{span}(S)$ then $S\cup \{w\}$ is linearly independent and $\mathrm{span}(S)⊊\mathrm{span}(S\cup \{w\})$; and if $w\in \mathrm{span}(S)$ then $\mathrm{span}(S\cup \{w\})=\mathrm{span}(S)$ is stated separately: it is the whole content of the step, and the same lemma does the same job in For $B\subseteq V$ the following are equivalent: $B$ is a basis; $B$ is a maximal linearly independent subset of $V$; $B$ is a minimal spanning subset of $V$ — maximality and minimality being in the inclusion order and in If ${\dim }_{F}V=n$ and $U$ is a linear subspace of $V$, then $U$ is finite-dimensional, ${\dim }_{F}U\le n$, and ${\dim }_{F}U=n$ if and only if $U=V$.