theorem :: NUMBER18:24

for m being Nat st m >= 1 & Fermat m is Prime holds
( card (PrimeDivisors (Fermat m)) = 1 & card (PrimeDivisors ((Fermat m) - 1)) = 1 )