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