ex B being Subset of V st
( {} the carrier of V c= B & B is linearly-independent & Lin B = VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) ) by Th22;
hence ex b₁ being Subset of V st
( b₁ is linearly-independent & Lin b₁ = VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) ) ; :: thesis: verum