theorem :: GR_CY_3:29

for p being Nat st p <> 1 & Mersenne p is Prime holds
p is Prime by Th28;