theorem Th15: :: HAUSDORF:15

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