8 = 2 * 4 ;
then A1: 2 divides 8 by NAT_D:def 3;
let p be Safe Prime; :: thesis: ( not p > 5 or p mod 8 = 3 or p mod 8 = 7 )
set k = p mod 8;
consider q being Prime such that
A2: (2 * q) + 1 = p by Def1;
assume A3: p > 5 ; :: thesis: ( p mod 8 = 3 or p mod 8 = 7 )

A4: now :: thesis: ( not p mod 8 = 0 & ... & not p mod 8 = 2 & not p mod 8 = 4 & ... & not p mod 8 = 6 )

assume A5: ( not not p mod 8 = 0 & ... & not p mod 8 = 2 or not not p mod 8 = 4 & ... & not p mod 8 = 6 ) ; :: thesis: contradiction

now :: thesis: contradiction

per cases ( p mod 8 = 0 or p mod 8 = 1 or p mod 8 = 2 or p mod 8 = 4 or p mod 8 = 5 or p mod 8 = 6 ) by A5;

suppose p mod 8 = 0 ; :: thesis: contradiction

then 8 divides p by INT_1:62;
then 2 divides p by A1, INT_2:9;
then 2 = p by INT_2:def 4;
hence contradiction by Th2; :: thesis: verum

end;

suppose p mod 8 = 1 ; :: thesis: contradiction

then ((p div 8) * 8) + 1 = (2 * q) + 1 by A2, INT_1:59;
then q = (p div 8) * 4 ;
then 4 divides q by INT_1:def 3;
hence contradiction by INT_2:29, INT_2:def 4; :: thesis: verum

end;

suppose p mod 8 = 2 ; :: thesis: contradiction

then p = ((p div 8) * 8) + 2 by INT_1:59
.= (((p div 8) * 4) + 1) * 2 ;
then 2 divides p by INT_1:def 3;
then 2 = p by INT_2:def 4;
hence contradiction by Th2; :: thesis: verum

end;

suppose p mod 8 = 4 ; :: thesis: contradiction

then p = ((p div 8) * 8) + 4 by INT_1:59
.= (((p div 8) * 4) + 2) * 2 ;
then 2 divides p by INT_1:def 3;
then 2 = p by INT_2:def 4;
hence contradiction by Th2; :: thesis: verum

end;

suppose p mod 8 = 5 ; :: thesis: contradiction

then ((p div 8) * 8) + 5 = (2 * q) + 1 by A2, INT_1:59;
then q = (((p div 8) * 2) + 1) * 2 ;
then 2 divides q by INT_1:def 3;
then 2 = q by INT_2:def 4;
hence contradiction by A3, A2; :: thesis: verum

end;

suppose p mod 8 = 6 ; :: thesis: contradiction

then p = ((p div 8) * 8) + 6 by INT_1:59
.= (((p div 8) * 4) + 3) * 2 ;
then 2 divides p by INT_1:def 3;
then 2 = p by INT_2:def 4;
hence contradiction by Th2; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

p mod 8 < 7 + 1 by NAT_D:62;
then p mod 8 <= 0 + 7 by NAT_1:13;
then not not p mod 8 = 0 & ... & not p mod 8 = 7 ;
hence ( p mod 8 = 3 or p mod 8 = 7 ) by A4; :: thesis: verum