for X being RealHilbertSpace
for M being Subspace of X
for x, x0 being Point of X
for d being Real st x0 in M & 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
( d = ||.(x - x0).|| iff for w being Point of X st w in M holds
w,x - x0 are_orthogonal )