for V being RealUnitarySpace
for W being Subspace of V holds
( ((0). V) /\ W = (0). V & W /\ ((0). V) = (0). V )