consider z being Element of M;
z -neighbour is Subset of M ;
hence ex b₁ being Subset of M ex x being Element of M st b₁ = x -neighbour ; :: thesis: verum