theorem Th17: :: RUSUB_7:17

for X being RealUnitarySpace
for M being Subspace of X
for x, m0 being Point of X st m0 in M holds
( ( for m being Point of X st m in M holds
||.(x - m0).|| <= ||.(x - m).|| ) iff for m being Point of X st m in M holds
(x - m0) .|. m = 0 )