:: deftheorem Def3 defines Basis RLVECT_3:def 3 :
for V being RealLinearSpace
for b₂ being Subset of V holds
( b₂ is Basis of V iff ( b₂ is linearly-independent & Lin b₂ = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) ) );