set y = the Element of M;
the Element of M -neighbour in { s where s is Subset of M : ex x being Element of M st x -neighbour = s } ;
hence not M -neighbour is empty ; :: thesis: verum