:: deftheorem defines Mersenne_Primes NUMBER18:def 6 :
Mersenne_Primes = { n where n is Prime : n is mersenne } ;