:: deftheorem Def1 defines Lin RUSUB_3:def 1 :
for V being RealUnitarySpace
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 } );