theorem :: GR_CY_3:26

for p being Sophie_Germain Prime st p > 2 & p mod 4 = 1 holds
ex q being Safe Prime st (Mersenne p) mod q = q - 2