theorem :: MOEBIUS1:39

for n, k being Nat holds
( k in NatDivisors n iff ( 0 < k & k divides n ) )