theorem Th25: :: RUSUB_7:25

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