theorem Th5: :: RUSUB_3:5

for V being RealUnitarySpace
for W being strict Subspace of V
for A being Subset of V st A = the carrier of W holds
Lin A = W