theorem Lm88: :: DUALSP04:31

for X being RealHilbertSpace
for M being Subspace of X
for N being Subset of X
for x being Point of X
for d being Real st N = the carrier of M & N is closed & ex Y being non empty Subset of REAL st
( Y = { ||.(x - y).|| where y is Point of X : y in M } & d = lower_bound Y & lower_bound Y >= 0 ) holds
ex x0 being Point of X st
( d = ||.(x - x0).|| & x0 in M )