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