let a, b, c, h be Integer; :: thesis:
assume A1: h = ((a - b) * (a - c)) * (b - c) ; :: thesis:
set r = numberR (a,b,c);
set r0 = numberR0 (a,b,c);
set SGM = Sgm (PrimeDivisors>3 h);
let S be Sierp45FS of a,b,c; :: thesis:
let n be Nat; :: thesis:
assume that
A2: a,b,c are_mutually_distinct and
A3: n, numberR (a,b,c) are_congruent_mod 2 and
A4: n, numberR0 (a,b,c) are_congruent_mod 3 and
A5: for i being Nat st i in dom S holds
n,S . i are_congruent_mod (Sgm (PrimeDivisors>3 h)) . i ; :: thesis:
assume A6: not a + n,c + n are_coprime ; :: thesis:
consider q being Prime such that
A7: ( q divides |.(a + n).| & q divides |.(c + n).| ) by A6, Th9, PYTHTRIP:def 2;
A8: ( q divides a + n & q divides c + n ) by A7, Th4;
then A9: q divides (a + n) - (c + n) by INT_5:1;
A10: h = (a - c) * ((a - b) * (b - c)) by A1;
two_or_more_are_odd_among a + n,b + n,c + n

numberR (a,b,c),n are_congruent_mod 2 by A3, INT_1:14;
then A11: ( a + (numberR (a,b,c)),a + n are_congruent_mod 2 & b + (numberR (a,b,c)),b + n are_congruent_mod 2 & c + (numberR (a,b,c)),c + n are_congruent_mod 2 ) ;
two_or_more_are_odd_among a + (numberR (a,b,c)),b + (numberR (a,b,c)),c + (numberR (a,b,c)) by Th33;
hence two_or_more_are_odd_among a + n,b + n,c + n by A11; :: thesis:

end;

then A12: q <> 2 by A8;
a + n,b + n,c + n at_least_two_are_not_divisible_by 3

A13: n mod 3 = (numberR0 (a,b,c)) mod 3 by A4, NAT_D:64;
A14: (a + (numberR0 (a,b,c))) mod 3 = ((a mod 3) + ((numberR0 (a,b,c)) mod 3)) mod 3 by NAT_D:66;
A15: (b + (numberR0 (a,b,c))) mod 3 = ((b mod 3) + ((numberR0 (a,b,c)) mod 3)) mod 3 by NAT_D:66;
A16: (c + (numberR0 (a,b,c))) mod 3 = ((c mod 3) + ((numberR0 (a,b,c)) mod 3)) mod 3 by NAT_D:66;
A17: (a + n) mod 3 = ((a mod 3) + (n mod 3)) mod 3 by NAT_D:66;
A18: (b + n) mod 3 = ((b mod 3) + (n mod 3)) mod 3 by NAT_D:66;
A19: (c + n) mod 3 = ((c mod 3) + (n mod 3)) mod 3 by NAT_D:66;

a + (numberR0 (a,b,c)),b + (numberR0 (a,b,c)),c + (numberR0 (a,b,c)) at_least_two_are_not_divisible_by 3 by Th34;

case ( not 3 divides a + (numberR0 (a,b,c)) & not 3 divides b + (numberR0 (a,b,c)) & 3 divides c + (numberR0 (a,b,c)) ) ; :: thesis:

then ( (a + (numberR0 (a,b,c))) mod 3 <> 0 & (b + (numberR0 (a,b,c))) mod 3 <> 0 & (c + (numberR0 (a,b,c))) mod 3 = 0 ) by INT_1:62;
hence ( not 3 divides a + n & not 3 divides b + n & 3 divides c + n ) by A13, A14, A15, A16, A17, A18, A19, INT_1:62; :: thesis:

end;

case ( not 3 divides a + (numberR0 (a,b,c)) & 3 divides b + (numberR0 (a,b,c)) & not 3 divides c + (numberR0 (a,b,c)) ) ; :: thesis:

then ( (a + (numberR0 (a,b,c))) mod 3 <> 0 & (b + (numberR0 (a,b,c))) mod 3 = 0 & (c + (numberR0 (a,b,c))) mod 3 <> 0 ) by INT_1:62;
hence ( not 3 divides a + n & 3 divides b + n & not 3 divides c + n ) by A13, A14, A15, A16, A17, A18, A19, INT_1:62; :: thesis:

end;

case ( 3 divides a + (numberR0 (a,b,c)) & not 3 divides b + (numberR0 (a,b,c)) & not 3 divides c + (numberR0 (a,b,c)) ) ; :: thesis:

then ( (a + (numberR0 (a,b,c))) mod 3 = 0 & (b + (numberR0 (a,b,c))) mod 3 <> 0 & (c + (numberR0 (a,b,c))) mod 3 <> 0 ) by INT_1:62;
hence ( 3 divides a + n & not 3 divides b + n & not 3 divides c + n ) by A13, A14, A15, A16, A17, A18, A19, INT_1:62; :: thesis:

end;

case ( not 3 divides a + (numberR0 (a,b,c)) & not 3 divides b + (numberR0 (a,b,c)) & not 3 divides c + (numberR0 (a,b,c)) ) ; :: thesis:

then ( (a + (numberR0 (a,b,c))) mod 3 <> 0 & (b + (numberR0 (a,b,c))) mod 3 <> 0 & (c + (numberR0 (a,b,c))) mod 3 <> 0 ) by INT_1:62;
hence ( not 3 divides a + n & not 3 divides b + n & not 3 divides c + n ) by A13, A14, A15, A16, A17, A18, A19, INT_1:62; :: thesis:

end;

end;

end;

hence a + n,b + n,c + n at_least_two_are_not_divisible_by 3 ; :: thesis:

end;

then A20: q <> 3 by A8;
consider h1 being Integer, F being FinSequence of NAT such that
A21: h1 = ((a - b) * (a - c)) * (b - c) and
A22: F = Sgm (PrimeDivisors>3 h1) and
A23: len S = len F and
A24: for i being object st i in dom S holds
( not F . i divides a + (S . i) & not F . i divides b + (S . i) & not F . i divides c + (S . i) ) by A2, Def12;
( a - b <> 0 & a - c <> 0 & b - c <> 0 ) by A2;
then A25: PrimeDivisors>3 h = rng (Sgm (PrimeDivisors>3 h)) by A1, FINSEQ_1:def 14;

assume q <= 3 ; :: thesis:
then not not q = 0 & ... & not q = 3 ;
hence contradiction by A12, A20, INT_2:def 4; :: thesis:

end;

then q in PrimeDivisors>3 h by A9, A10, Th38, INT_2:2;
then consider i being object such that
A26: i in dom (Sgm (PrimeDivisors>3 h)) and
A27: q = (Sgm (PrimeDivisors>3 h)) . i by A25, FUNCT_1:def 3;
reconsider i = i as Nat by A26;
A28: dom S = dom (Sgm (PrimeDivisors>3 h)) by A1, A21, A22, A23, FINSEQ_3:29;
then n,S . i are_congruent_mod q by A5, A26, A27;
then A29: n + a,(S . i) + a are_congruent_mod q ;
( not q divides a + (S . i) & not q divides b + (S . i) & not q divides c + (S . i) ) by A1, A21, A22, A26, A27, A28, A24;
hence contradiction by A8, A29, Th19; :: thesis: