for n being non zero Nat holds
( Top (Divisors_Lattice n) = n & Bottom (Divisors_Lattice n) = 1 )