:: deftheorem Def2 defines /\ RUSUB_2:def 2 :
for V being RealUnitarySpace
for W1, W2 being Subspace of V
for b₄ being strict Subspace of V holds
( b₄ = W1 /\ W2 iff the carrier of b₄ = the carrier of W1 /\ the carrier of W2 );