theorem Th19: :: HAUSDORF:19

for M being non empty MetrSpace
for P being non empty Subset of (TopSpaceMetr M)
for z being Point of M ex w being Point of M st
( w in P & (dist_min P) . z <= dist (w,z) )