theorem Th8: :: METRIC_2:8

for M being PseudoMetricSpace
for x, y being Element of M holds
( x -neighbour = y -neighbour iff x tolerates y ) by Th2, Th4, Th7;