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