let M be PseudoMetricSpace; :: thesis: for x, y being Element of M holds
( x -neighbour = y -neighbour iff x tolerates y )
let x, y be Element of M; :: thesis: ( x -neighbour = y -neighbour iff x tolerates y )

hereby :: thesis: ( x tolerates y implies x -neighbour = y -neighbour )

assume x -neighbour = y -neighbour ; :: thesis: x tolerates y
then x in y -neighbour by Th9;
hence x tolerates y by Th7; :: thesis: verum

end;

assume x tolerates y ; :: thesis: x -neighbour = y -neighbour
then x in y -neighbour ;
hence x -neighbour = y -neighbour by Th12; :: thesis: verum