let M be PseudoMetricSpace; :: thesis: for x, y being Element of M holds
( x -neighbour meets y -neighbour iff x tolerates y )
let x, y be Element of M; :: thesis: ( x -neighbour meets y -neighbour iff x tolerates y )

hereby :: thesis: ( x tolerates y implies x -neighbour meets y -neighbour )

assume x -neighbour meets y -neighbour ; :: thesis: x tolerates y
then consider p being set such that
A1: ( p in x -neighbour & p in y -neighbour ) by XBOOLE_0:3;
A2: ex q being Element of M st
( q = p & x tolerates q ) by A1;
reconsider p = p as Element of M by A1;
ex s being Element of M st
( s = p & y tolerates s ) by A1;
hence x tolerates y by A2, Th6; :: thesis: verum

end;

assume x tolerates y ; :: thesis: x -neighbour meets y -neighbour
then A3: x in y -neighbour ;
x in x -neighbour by Th9;
hence x -neighbour meets y -neighbour by A3, XBOOLE_0:3; :: thesis: verum