for V being RealUnitarySpace
for W being strict Subspace of V holds W /\ W = W