theorem Th18: :: DUALSP06:18

for X being RealNormSpace
for x being Point of X
for M being non empty Subspace of X holds { ||.(x - m).|| where m is Point of X : m in M } is non empty real-membered bounded_below set