:: deftheorem defines Fermat PEPIN:def 3 :
for n being Nat holds Fermat n = (2 |^ (2 |^ n)) + 1;