theorem Th19: :: RUSUB_7:19

for X being RealHilbertSpace
for M being Subspace of X
for x being Point of X st the carrier of M is closed Subset of (TopSpaceNorm (RUSp2RNSp X)) holds
ex m0 being Point of X st
( m0 in M & ( for m being Point of X st m in M holds
||.(x - m0).|| <= ||.(x - m).|| ) )