theorem Th13: :: HAUSDORF:13

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