theorem Th9: :: HAUSDORF:9

for M being non empty MetrSpace
for P being non empty closed Subset of (TopSpaceMetr M)
for x being Point of M holds
( x in P iff (dist_min P) . x = 0 )