let V be set ; :: thesis: for M being non empty MetrSpace holds
( V in M -neighbour iff ex x being Element of M st V = {x} )
let M be non empty MetrSpace; :: thesis: ( V in M -neighbour iff ex x being Element of M st V = {x} )
A1: ( V in M -neighbour implies ex x being Element of M st V = {x} )
proof
assume V in M -neighbour ; :: thesis: ex x being Element of M st V = {x}
then consider x being Element of M such that
A2: V = x -neighbour by Th15;
x -neighbour = {x} by Th13;
hence ex x being Element of M st V = {x} by A2; :: thesis: verum
end;
( ex x being Element of M st V = {x} implies V in M -neighbour )
proof
given x being Element of M such that A3: V = {x} ; :: thesis: V in M -neighbour
x -neighbour = {x} by Th13;
hence V in M -neighbour by A3; :: thesis: verum
end;
hence ( V in M -neighbour iff ex x being Element of M st V = {x} ) by A1; :: thesis: verum