theorem DivInPlus: :: MOEBIUS2:58

for n being non zero Nat holds NatDivisors n c= NATPLUS by NAT_LAT:def 6;