theorem Th4: :: HAUSDORF:4

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