theorem :: GR_CY_3:8
for p being Safe Prime holds
( not p > 5 or p mod 8 = 3 or p mod 8 = 7 )