theorem Th3: :: HAUSDORF:3

for M being non empty MetrSpace
for P being Subset of (TopSpaceMetr M)
for x being Point of M st x in P holds
0 in (dist x) .: P