let M be PseudoMetricSpace; :: thesis: for x, y being Element of M st x in y -neighbour holds
y in x -neighbour
let x, y be Element of M; :: thesis: ( x in y -neighbour implies y in x -neighbour )
assume x in y -neighbour ; :: thesis: y in x -neighbour
then x tolerates y by Th2;
hence y in x -neighbour ; :: thesis: verum