let M be non empty MetrSpace; :: thesis: for x, y being Element of M holds
( y in x -neighbour iff y = x )
let x, y be Element of M; :: thesis: ( y in x -neighbour iff y = x )

hereby :: thesis: ( y = x implies y in x -neighbour )

assume y in x -neighbour ; :: thesis: y = x
then ex q being Element of M st
( y = q & x tolerates q ) ;
hence y = x by Th11; :: thesis: verum

end;

assume y = x ; :: thesis: y in x -neighbour
then x tolerates y by Th11;
hence y in x -neighbour ; :: thesis: verum