:: deftheorem Def12 defines mersenne NUMPOLY1:def 12 :
for n being number holds
( n is mersenne iff ex p being Nat st n = Mersenne p );