theorem Th7: :: RLSUB_2:7
for V being RealLinearSpace
for W1, W2 being Subspace of V holds
( W1 is Subspace of W1 + W2 & W2 is Subspace of W1 + W2 )