{} the carrier of V is linearly-independent by RLVECT_3:7;
then ex B being Subset of V st
( {} the carrier of V c= B & B is linearly-independent & Lin B = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) ) by Th11;
hence ex b₁ being Subset of V st
( b₁ is linearly-independent & Lin b₁ = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) ) ; :: thesis: verum