:: deftheorem defines NatDivisors MOEBIUS1:def 4 :
for n being Nat holds NatDivisors n = { k where k is Element of NAT : ( k <> 0 & k divides n ) } ;