theorem :: RUSUB_2:4

for V being RealUnitarySpace
for W being strict Subspace of V holds W + W = W by Lm3;