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 object such that
A1: p in x -neighbour and
A2: p in y -neighbour by XBOOLE_0:3;
A3: 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 A2;
hence x tolerates y by A3, Th1; :: thesis: verum
end;
assume x tolerates y ; :: thesis: x -neighbour meets y -neighbour
then A4: x in y -neighbour ;
x in x -neighbour by Th4;
hence x -neighbour meets y -neighbour by A4, XBOOLE_0:3; :: thesis: verum