let p be Safe Prime; :: thesis: ( p > 7 implies p mod 12 = 11 )
assume A1: p > 7 ; :: thesis: p mod 12 = 11
then p > 7 - 2 by XREAL_1:51;
then A2: p mod 4 = 3 by Th5;
A3: (9 * p) mod 12 = (3 * (3 * p)) mod (3 * 4)
.= 3 * ((3 * p) mod 4) by INT_4:20
.= 3 * (((3 mod 4) * (p mod 4)) mod 4) by NAT_D:67
.= 3 * ((3 * 3) mod 4) by A2, NAT_D:24
.= 3 * ((1 + (4 * 2)) mod 4)
.= 3 * (1 mod 4) by NAT_D:61
.= 3 * 1 by PEPIN:5 ;
A4: (4 * p) mod 12 = (4 * p) mod (4 * 3)
.= 4 * (p mod 3) by INT_4:20
.= 4 * 2 by A1, Th4 ;
p mod 12 = (p + (12 * p)) mod 12 by NAT_D:61
.= ((4 * p) + (9 * p)) mod 12
.= ((4 * 2) + (3 * 1)) mod 12 by A4, A3, NAT_D:66
.= 11 by NAT_D:24 ;
hence p mod 12 = 11 ; :: thesis: verum