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

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

assume y in x -neighbour ; :: thesis: y tolerates x
then ex q being Element of M st
( y = q & x tolerates q ) ;
hence y tolerates x ; :: thesis: verum

end;

assume y tolerates x ; :: thesis: y in x -neighbour
hence y in x -neighbour ; :: thesis: verum