:: deftheorem defines Mersenne GR_CY_3:def 3 :
for n being Nat holds Mersenne n = (2 |^ n) - 1;