let V be set ; :: thesis: for M being non empty MetrStruct holds
( V in M -neighbour iff ex x being Element of M st V = x -neighbour )
let M be non empty MetrStruct ; :: thesis: ( V in M -neighbour iff ex x being Element of M st V = x -neighbour )
( V in M -neighbour implies ex x being Element of M st V = x -neighbour )

proof

assume V in M -neighbour ; :: thesis: ex x being Element of M st V = x -neighbour
then ex q being Subset of M st
( q = V & ex x being Element of M st q = x -neighbour ) ;
hence ex x being Element of M st V = x -neighbour ; :: thesis: verum

end;

hence ( V in M -neighbour iff ex x being Element of M st V = x -neighbour ) ; :: thesis: verum