theorem Th2: :: HAUSDORF:2

for M being non empty MetrSpace
for x being Point of M holds (dist x) . x = 0