let M be PseudoMetricSpace; :: thesis: for x being Element of holds x in x -neighbour
let x be Element of ; :: thesis: x in x -neighbour
x tolerates x by Lm1;
hence x in x -neighbour ; :: thesis: verum