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