:: deftheorem defines LC_RLSpace RLVECT_2:def 20 :
for V being RealLinearSpace
for A being Subset of V
for b₃ being strict Subspace of LC_RLSpace V holds
( b₃ = LC_RLSpace A iff the carrier of b₃ = { l where l is Linear_Combination of A : verum } );