:: deftheorem Def3 defines Subspaces RLSUB_2:def 3 :
for V being RealLinearSpace
for b₂ being set holds
( b₂ = Subspaces V iff for x being object holds
( x in b₂ iff x is strict Subspace of V ) );