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 ( p in x -neighbour & x tolerates y ) ; :: thesis: p in y -neighbour
then ( p tolerates x & x tolerates y ) by Th7;
then p tolerates y by Th6;
hence p in y -neighbour ; :: thesis: verum