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