consider y being Element of M;
y -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