:: deftheorem Def1 defines Safe GR_CY_3:def 1 :
for p being Nat holds
( p is Safe iff ex sgp being Prime st (2 * sgp) + 1 = p );