let
p
be
Safe
Prime
;
:: thesis:
p
mod
2
=
1
p
>=
4
+
1
by
Th2
;
then
p
>
4
by
NAT_1:13
;
then
p
>
4

2
by
XREAL_1:51
;
then
p
is
odd
by
PEPIN:17
;
hence
p
mod
2
=
1
by
NAT_2:22
;
:: thesis:
verum