let M be PseudoMetricSpace; :: thesis: for x, y being Element of M st y in x -neighbour holds
x -neighbour = y -neighbour
let x, y be Element of M; :: thesis: ( y in x -neighbour implies x -neighbour = y -neighbour )
assume A1: y in x -neighbour ; :: thesis: x -neighbour = y -neighbour
A2: for p being Element of M st p in x -neighbour holds
p in y -neighbour

proof

let p be Element of M; :: thesis: ( p in x -neighbour implies p in y -neighbour )
assume p in x -neighbour ; :: thesis: p in y -neighbour
then ( p tolerates x & x tolerates y ) by A1, Th7;
then p tolerates y by Th6;
hence p in y -neighbour ; :: thesis: verum

end;

for p being Element of M st p in y -neighbour holds
p in x -neighbour

proof

let p be Element of M; :: thesis: ( p in y -neighbour implies p in x -neighbour )
assume p in y -neighbour ; :: thesis: p in x -neighbour
then ( p tolerates y & y tolerates x ) by A1, Th7;
then p tolerates x by Th6;
hence p in x -neighbour ; :: thesis: verum

end;

then ( x -neighbour c= y -neighbour & y -neighbour c= x -neighbour ) by A2, SUBSET_1:7;
hence x -neighbour = y -neighbour by XBOOLE_0:def 10; :: thesis: verum