for V being RealUnitarySpace
for W1, W2 being Subspace of V holds
( ( W1 is Subspace of W2 or W2 is Subspace of W1 ) iff ex W being Subspace of V st the carrier of W = the carrier of W1 \/ the carrier of W2 )