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