theorem :: RLSUB_2:4

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