theorem Th20: :: RUSUB_2:20

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