:: deftheorem Def2 defines (0). RUSUB_1:def 2 :
for V being RealUnitarySpace
for b₂ being strict Subspace of V holds
( b₂ = (0). V iff the carrier of b₂ = {(0. V)} );