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