reconsider p = 5 as Prime by PEPIN:64;
reconsider sgp = 2 as Prime by INT_2:44;
take sgp ; :: thesis: sgp is Sophie_Germain
p = (2 * sgp) + 1 ;
hence sgp is Sophie_Germain by Def2; :: thesis: verum