:: deftheorem defines Fermat_Primes NUMBER18:def 8 :
Fermat_Primes = { n where n is Prime : n is fermat } ;