theorem :: RUSUB_1:35

for V being strict RealUnitarySpace holds V is Subspace of (Omega). V ;