theorem OnlyPrimeDiv2: :: NUMBER18:41

for n being odd Nat st card (PrimeDivisors n) = 1 holds
ex k being Nat ex p being Prime st n = p |^ k