NatDivisors n is finite ;
hence Divisors_Lattice n is finite by MOEBIUS2:def 10; :: thesis: verum