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