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

A3: now :: thesis: ( not p mod 3 = 0 & not p mod 3 = 1 )

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

now :: thesis: contradiction

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

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

then 3 divides p by INT_1:62;
then 3 = p by INT_2:def 4;
hence contradiction by Th2; :: thesis: verum

end;

suppose A5: p mod 3 = 1 ; :: thesis: contradiction

2,3 are_coprime by INT_2:28, INT_2:30, PEPIN:41;
then A6: 2 gcd 3 = 1 by INT_2:def 3;
3 divides ((2 * q) + 1) - 1 by A1, A5, PEPIN:8;
then 3 divides q by A6, WSIERP_1:29;
then 3 = q by INT_2:def 4;
hence contradiction by A2, A1; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

p mod 3 < 2 + 1 by NAT_D:62;
then p mod 3 <= 0 + 2 by NAT_1:13;
then not not p mod 3 = 0 & ... & not p mod 3 = 2 ;
hence p mod 3 = 2 by A3; :: thesis: verum