theorem :: GR_CY_3:24

for p being Prime st p <> 2 holds
(Mersenne p) mod 8 = 7