let m1, m2, c2, c1 be Integer; :: thesis: ( m1 <> 0 & m2 <> 0 & m1 gcd m2 divides c2 - c1 implies ex r being Integer st
( ( for x being Integer st (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 holds
x,c1 + (m1 * r) are_congruent_mod m1 lcm m2 ) & (((m1 div (m1 gcd m2)) * r) - ((c2 - c1) div (m1 gcd m2))) mod (m2 div (m1 gcd m2)) = 0 ) )
assume A1: ( m1 <> 0 & m2 <> 0 & m1 gcd m2 divides c2 - c1 ) ; :: thesis: ex r being Integer st
( ( for x being Integer st (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 holds
x,c1 + (m1 * r) are_congruent_mod m1 lcm m2 ) & (((m1 div (m1 gcd m2)) * r) - ((c2 - c1) div (m1 gcd m2))) mod (m2 div (m1 gcd m2)) = 0 )
A2: ( m1 = (m1 div (m1 gcd m2)) * (m1 gcd m2) & m2 = (m2 div (m1 gcd m2)) * (m1 gcd m2) ) by Lm11, INT_2:31;
set d = m1 gcd m2;
set d1 = m1 div (m1 gcd m2);
set d2 = m2 div (m1 gcd m2);
set d3 = (c2 - c1) div (m1 gcd m2);
A3: m1 gcd m2 <> 0 by A1, INT_2:35;
A4: m1 div (m1 gcd m2),m2 div (m1 gcd m2) are_relative_prime by A1, Lm12;
then consider r being Integer such that
A5: (((m1 div (m1 gcd m2)) * r) - ((c2 - c1) div (m1 gcd m2))) mod (m2 div (m1 gcd m2)) = 0 by Th15;
A6: for x being Integer st (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 holds
x,c1 + (m1 * r) are_congruent_mod m1 lcm m2

proof

let x be Integer; :: thesis: ( (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 implies x,c1 + (m1 * r) are_congruent_mod m1 lcm m2 )
assume A7: ( (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 ) ; :: thesis: x,c1 + (m1 * r) are_congruent_mod m1 lcm m2
A8: x - c1 = (((x - c1) div m1) * m1) + ((x - c1) mod m1) by A1, INT_1:86
.= ((x - c1) div m1) * m1 by A7 ;
then x - ((m1 * r) + c1) = m1 * (((x - c1) div m1) - r) ;
then A9: m1 divides x - ((m1 * r) + c1) by INT_1:def 9;
set y = (x - c1) div m1;
(x - c2) mod m2 = ((m1 * ((x - c1) div m1)) - (c2 - c1)) mod m2 by A8
.= ((((m1 gcd m2) * (m1 div (m1 gcd m2))) * ((x - c1) div m1)) - ((m1 gcd m2) * ((c2 - c1) div (m1 gcd m2)))) mod ((m1 gcd m2) * (m2 div (m1 gcd m2))) by A1, A2, Lm11 ;
then (m2 div (m1 gcd m2)) * (m1 gcd m2) divides (((m1 div (m1 gcd m2)) * ((x - c1) div m1)) - ((c2 - c1) div (m1 gcd m2))) * (m1 gcd m2) by A1, A2, A7, Lm10;
then m2 div (m1 gcd m2) divides ((m1 div (m1 gcd m2)) * ((x - c1) div m1)) - ((c2 - c1) div (m1 gcd m2)) by A3, Th7;
then A10: (((m1 div (m1 gcd m2)) * ((x - c1) div m1)) - ((c2 - c1) div (m1 gcd m2))) mod (m2 div (m1 gcd m2)) = 0 by Lm10;
m2 div (m1 gcd m2) <> 0 by A1, A2;
then r in Class (Cong (m2 div (m1 gcd m2))),((x - c1) div m1) by A4, A5, A10, Th26;
then [((x - c1) div m1),r] in Cong (m2 div (m1 gcd m2)) by EQREL_1:26;
then (x - c1) div m1,r are_congruent_mod m2 div (m1 gcd m2) by Def1;
then m2 div (m1 gcd m2) divides ((x - c1) div m1) - r by INT_2:19;
then consider w being Integer such that
A11: ((x - c1) div m1) - r = (m2 div (m1 gcd m2)) * w by INT_1:def 9;
x = c1 + (((x - c1) div m1) * m1) by A8
.= c1 + ((((m2 div (m1 gcd m2)) * w) + r) * m1) by A11
.= ((m1 * r) + c1) + ((w * (m1 div (m1 gcd m2))) * m2) by A2 ;
then m2 divides x - ((m1 * r) + c1) by INT_1:def 9;
then m1 lcm m2 divides x - ((m1 * r) + c1) by A9, INT_2:27;
hence x,c1 + (m1 * r) are_congruent_mod m1 lcm m2 by INT_2:19; :: thesis: verum

end;

take r ; :: thesis: ( ( for x being Integer st (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 holds
x,c1 + (m1 * r) are_congruent_mod m1 lcm m2 ) & (((m1 div (m1 gcd m2)) * r) - ((c2 - c1) div (m1 gcd m2))) mod (m2 div (m1 gcd m2)) = 0 )
thus ( ( for x being Integer st (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 holds
x,c1 + (m1 * r) are_congruent_mod m1 lcm m2 ) & (((m1 div (m1 gcd m2)) * r) - ((c2 - c1) div (m1 gcd m2))) mod (m2 div (m1 gcd m2)) = 0 ) by A5, A6; :: thesis: verum