The following quoted text is from Evar D. Nering's Linear Algebra and Matrix Theory, 2nd Ed.
Theorem 3.5. In a finite dimensional vector space, every spanning set contains a basis.
Proof: Let $\mathcal{B}$ be a set spanning $\mathcal{V}$. If $\mathcal{V}=\{0\}$, then $\emptyset\subset\mathcal{B}$ is a basis of $\{0\}$. If $\mathcal{V}\ne\{0\}$ then $\mathcal{B}$ must contain at least one non-zero vector $\alpha_{1}$. We now search for another vector in $\mathcal{B}$ which is not dependent on $\{\alpha_{1}\}$. We call this vector $\alpha_{2}$ and search for another vector in $\mathcal{B}$ which is not dependent on the linearly independent set $\{\alpha_{1},\alpha_{2}\}$. We continue in this way as long as we can, but the process must terminate as we cannot find more than $n$ linearly independent vectors in $\mathcal{B}$. Thus suppose we have obtained the set $\mathcal{A}=\{\alpha_{1},\dots,\alpha_{n}\}$ with the property that every vector in $\mathcal{B}$ is linearly dependent on $\mathcal{A}$. Then because of Theorem 2.1 the set $\mathcal{A}$ must also span $\mathcal{V}$ and it is a basis.
The reasoning in the proof seems circular. "Seek, and ye shall find." isn't very rigorous. I certainly believe that I could find such linearly independent vectors, but that's because I believe the theorem to be true.
Is the proof satisfactory?
I might be able to come up with my own proof, but I would still like to know if Nering's proof is satisfactory to mathematicians.