:: deftheorem FerDef defines fermat NUMBER18:def 7 :
for n being Nat holds
( n is fermat iff ex k being Nat st n = Fermat k );