theorem :: RUSUB_2:33

for V being strict RealUnitarySpace holds V in Subspaces V