let
p
be
Safe
Prime
;
:: thesis:
p
>=
5
consider
q
being
Prime
such that
A1
:
(
2
*
q
)
+
1
=
p
by
Def1
;
q
>
1
by
INT_2:def 4
;
then
q
>=
1
+
1
by
NAT_1:13
;
then
2
*
q
>=
2
*
2
by
XREAL_1:64
;
then
(
2
*
q
)
+
1
>=
4
+
1
by
XREAL_1:7
;
hence
p
>=
5
by
A1
;
:: thesis:
verum