theorem Th8: :: RUSUB_2:8

for V being RealUnitarySpace
for W1 being Subspace of V
for W2 being strict Subspace of V holds
( W1 is Subspace of W2 iff W1 + W2 = W2 )