:: deftheorem Def3 defines (0). RLSUB_1:def 3 :
for V being RealLinearSpace
for b₂ being strict Subspace of V holds
( b₂ = (0). V iff the carrier of b₂ = {(0. V)} );