theorem Th3: :: RUSUB_1:3

for V being RealUnitarySpace
for W being Subspace of V
for w being VECTOR of W holds w is VECTOR of V