theorem :: LATSTONE:26

for p being Prime holds NatDivisors p = {1,p}