theorem Th26: :: RUSUB_7:26

for X being RealHilbertSpace
for M being strict Subspace of X st X is strict & the carrier of M is closed Subset of (TopSpaceNorm (RUSp2RNSp X)) holds
M = Ort_Comp (Ort_Comp M)