theorem Th10: :: METRIC_2:10

for M being PseudoMetricSpace
for x, p, q being Element of M st p in x -neighbour & q in x -neighbour holds
dist (p,q) = 0