reconsider n = 1 as non zero Nat ;
Divisors_Lattice n is Boolean by MOEBIUS1:22;
hence ex b₁ being Boolean Lattice st b₁ is complete ; :: thesis: verum