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