let a be Element of (Divisors_Lattice n); :: thesis: not a is zero
a in the carrier of (Divisors_Lattice n) ;
then a in NatDivisors n by DivLat;
hence not a is zero ; :: thesis: verum