theorem Th2: :: RUSUB_2:2

for V being RealUnitarySpace
for W1, W2 being Subspace of V
for v being VECTOR of V st ( v in W1 or v in W2 ) holds
v in W1 + W2