theorem Th10: :: RLSUB_1:10
for V being RealLinearSpace
for W being Subspace of V
for w being VECTOR of W holds w is VECTOR of V