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
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 A2: p tolerates y by Th2;
y tolerates x by A1, Th2;
then p tolerates x by A2, Th1;
hence p in x -neighbour ; :: thesis: verum

end;

then A3: y -neighbour c= x -neighbour by SUBSET_1:2;
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 A4: p tolerates x by Th2;
x tolerates y by A1, Th2;
then p tolerates y by A4, Th1;
hence p in y -neighbour ; :: thesis: verum

end;

then x -neighbour c= y -neighbour by SUBSET_1:2;
hence x -neighbour = y -neighbour by A3, XBOOLE_0:def 10; :: thesis: verum