theorem Th14: :: HAUSDORF:14

for M being non empty MetrSpace
for P being non empty Subset of (TopSpaceMetr M)
for r being Real
for x being Point of M st ( for y being Point of M st y in P holds
dist (x,y) >= r ) holds
(dist_min P) . x >= r