let p be Safe Prime; :: thesis: ( p <> 5 implies p mod 4 = 3 )
set k = p mod 4;
consider q being Prime such that
A1: (2 * q) + 1 = p by Def1;
assume A2: p <> 5 ; :: thesis: p mod 4 = 3

A3: now

assume A4: ( p mod 4 = 0 or p mod 4 = 1 or p mod 4 = 2 ) ; :: thesis: contradiction

now

per cases ( p mod 4 = 0 or p mod 4 = 1 or p mod 4 = 2 ) by A4;

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

then 4 divides p by INT_1:89;
hence contradiction by INT_2:46, INT_2:def 5; :: thesis: verum

end;

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

then ((p div 4) * 4) + 1 = (2 * q) + 1 by A1, INT_1:86;
then q = (p div 4) * 2 ;
then 2 divides q by INT_1:def 9;
then 2 = q by INT_2:def 5;
hence contradiction by A2, A1; :: thesis: verum

end;

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

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

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

p mod 4 < 3 + 1 by INT_3:9;
then p mod 4 <= 0 + 3 by NAT_1:13;
hence p mod 4 = 3 by A3, NAT_1:28; :: thesis: verum