:: deftheorem DivLat defines Divisors_Lattice MOEBIUS2:def 10 :
for n being non zero Nat
for b₂ being strict SubLattice of NatPlus_Lattice holds
( b₂ = Divisors_Lattice n iff the carrier of b₂ = NatDivisors n );