the carrier of (Divisors_Lattice n) = NatDivisors n by DivLat;
hence the carrier of (Divisors_Lattice n) is natural-membered ; :: thesis: verum