theorem :: NUMBER12:46

for n being non zero Nat holds PrimeDivisors n c= Seg n