let M be non empty MetrSpace; :: thesis: for x being Element of M holds x -neighbour = {x}
let x be Element of M; :: thesis: x -neighbour = {x}
for p being Element of M st p in {x} holds
p in x -neighbour

proof

let p be Element of M; :: thesis: ( p in {x} implies p in x -neighbour )
assume p in {x} ; :: thesis: p in x -neighbour
then p = x by TARSKI:def 1;
hence p in x -neighbour by Th12; :: thesis: verum

end;

then A1: {x} c= x -neighbour by SUBSET_1:2;
for p being Element of M st p in x -neighbour holds
p in {x}

proof

let p be Element of M; :: thesis: ( p in x -neighbour implies p in {x} )
assume p in x -neighbour ; :: thesis: p in {x}
then p = x by Th12;
hence p in {x} by TARSKI:def 1; :: thesis: verum

end;

then x -neighbour c= {x} by SUBSET_1:2;
hence x -neighbour = {x} by A1, XBOOLE_0:def 10; :: thesis: verum