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