:: deftheorem Def2 defines Sophie_Germain GR_CY_3:def 2 :
for p being Nat holds
( p is Sophie_Germain iff (2 * p) + 1 is Prime );