let a, b, c, h be Integer; :: thesis:
assume A1: h = ((a - b) * (a - c)) * (b - c) ; :: thesis:
let S be Sierp45FS of a,b,c; :: thesis:
assume A2: a,b,c are_mutually_distinct ; :: thesis:
let n be Nat; :: thesis:
assume that
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 not a + n,b + n,c + n are_mutually_coprime ; :: thesis:

suppose not a + n,b + n are_coprime ; :: thesis:

hence contradiction by A1, A2, A3, A4, A5, Lm7; :: thesis:

end;

suppose not a + n,c + n are_coprime ; :: thesis:

hence contradiction by A1, A2, A3, A4, A5, Lm8; :: thesis:

end;

suppose not b + n,c + n are_coprime ; :: thesis:

hence contradiction by A1, A2, A3, A4, A5, Lm9; :: thesis:

end;

end;