theorem Th8: :: RLSUB_2:8

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