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