theorem :: NUMBER12:47

for n being Nat holds PrimeDivisors n c= NatDivisors n