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