theorem OnlyPrimeDiv: :: NUMBER18:42

for n being even Nat st card (PrimeDivisors n) = 1 holds
ex k being Nat st n = 2 |^ k