theorem Th2: :: RUSUB_1:2

for V being RealUnitarySpace
for W being Subspace of V
for x being object st x in W holds
x in V