set h = ((a - b) * (a - c)) * (b - c);
set F = Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c)));
A2: Seg (len (Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c))))) = dom (Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c)))) by FINSEQ_1:def 3;
defpred S₁[ object , Integer] means ( not (Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c)))) . $1 divides a + $2 & not (Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c)))) . $1 divides b + $2 & not (Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c)))) . $1 divides c + $2 );
A3: for i being Nat st i in Seg (len (Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c))))) holds
ex x being Element of INT st S₁[i,x]

proof

let i be Nat; :: thesis: ( i in Seg (len (Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c))))) implies ex x being Element of INT st S₁[i,x] )
assume A4: i in Seg (len (Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c))))) ; :: thesis: ex x being Element of INT st S₁[i,x]
set n = (Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c)))) . i;
A5: ( a - b <> 0 & a - c <> 0 & b - c <> 0 ) by A1;
(Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c)))) . i in rng (Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c)))) by A2, A4, FUNCT_1:def 3;
then (Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c)))) . i in PrimeDivisors>3 (((a - b) * (a - c)) * (b - c)) by A5, FINSEQ_1:def 14;
then consider k being Integer such that
A6: ( not (Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c)))) . i divides k + a & not (Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c)))) . i divides k + b & not (Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c)))) . i divides k + c ) by Th35, NUMBER03:53;
reconsider k = k as Element of INT by INT_1:def 2;
take k ; :: thesis: S₁[i,k]
thus S₁[i,k] by A6; :: thesis: verum

end;

consider p being FinSequence of INT such that
A7: dom p = Seg (len (Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c))))) and
A8: for k being Nat st k in Seg (len (Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c))))) holds
S₁[k,p . k] from FINSEQ_1:sch 5(A3);
take p ; :: thesis: ex h being Integer ex F being FinSequence of NAT st
( h = ((a - b) * (a - c)) * (b - c) & F = Sgm (PrimeDivisors>3 h) & len p = len F & ( for i being object st i in dom p holds
( not F . i divides a + (p . i) & not F . i divides b + (p . i) & not F . i divides c + (p . i) ) ) )
take ((a - b) * (a - c)) * (b - c) ; :: thesis: ex F being FinSequence of NAT st
( ((a - b) * (a - c)) * (b - c) = ((a - b) * (a - c)) * (b - c) & F = Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c))) & len p = len F & ( for i being object st i in dom p holds
( not F . i divides a + (p . i) & not F . i divides b + (p . i) & not F . i divides c + (p . i) ) ) )
take Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c))) ; :: thesis: ( ((a - b) * (a - c)) * (b - c) = ((a - b) * (a - c)) * (b - c) & Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c))) = Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c))) & len p = len (Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c)))) & ( for i being object st i in dom p holds
( not (Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c)))) . i divides a + (p . i) & not (Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c)))) . i divides b + (p . i) & not (Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c)))) . i divides c + (p . i) ) ) )
thus ((a - b) * (a - c)) * (b - c) = ((a - b) * (a - c)) * (b - c) ; :: thesis: ( Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c))) = Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c))) & len p = len (Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c)))) & ( for i being object st i in dom p holds
( not (Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c)))) . i divides a + (p . i) & not (Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c)))) . i divides b + (p . i) & not (Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c)))) . i divides c + (p . i) ) ) )
thus Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c))) = Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c))) ; :: thesis: ( len p = len (Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c)))) & ( for i being object st i in dom p holds
( not (Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c)))) . i divides a + (p . i) & not (Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c)))) . i divides b + (p . i) & not (Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c)))) . i divides c + (p . i) ) ) )
thus len p = len (Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c)))) by A7, FINSEQ_1:def 3; :: thesis: for i being object st i in dom p holds
( not (Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c)))) . i divides a + (p . i) & not (Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c)))) . i divides b + (p . i) & not (Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c)))) . i divides c + (p . i) )
thus for i being object st i in dom p holds
( not (Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c)))) . i divides a + (p . i) & not (Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c)))) . i divides b + (p . i) & not (Sgm (PrimeDivisors>3 (((a - b) * (a - c)) * (b - c)))) . i divides c + (p . i) ) by A7, A8; :: thesis: verum