:: deftheorem Def2 defines Lin RLVECT_3:def 2 :
for V being RealLinearSpace
for A being Subset of V
for b₃ being strict Subspace of V holds
( b₃ = Lin A iff the carrier of b₃ = { (Sum l) where l is Linear_Combination of A : verum } );