theorem Th27: :: HAUSDORF:27

for M being non empty MetrSpace
for P being non empty Subset of (TopSpaceMetr M) holds (dist_min P) .: P = {0}