theorem :: GR_CY_3:9

for p being Sophie_Germain Prime holds
( not p > 2 or p mod 4 = 1 or p mod 4 = 3 )