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 Th7;
then p tolerates q by Th6;
hence dist p,q = 0 by Def1; :: thesis: verum