let m1, m2, c1, c2 be Integer; :: thesis:
assume A1: ( m1 <> 0 & m2 <> 0 & m1,m2 are_relative_prime ) ; :: thesis:
then consider r being Integer such that
A2: ((m1 * r) - (c2 - c1)) mod m2 = 0 by Th15;
A3: for x being Integer st (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 holds
x,c1 + (m1 * r) are_congruent_mod m1 * m2

let x be Integer; :: thesis:
assume A4: ( (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 ) ; :: thesis:
A5: x - c1 = (((x - c1) div m1) * m1) + ((x - c1) mod m1) by A1, INT_1:86
.= ((x - c1) div m1) * m1 by A4 ;
set y = (x - c1) div m1;
(x - c2) mod m2 = ((m1 * ((x - c1) div m1)) - (c2 - c1)) mod m2 by A5;
then (x - c1) div m1 in Class (Cong m2),r by A1, A2, A4, Th26;
then [r,((x - c1) div m1)] in Cong m2 by EQREL_1:26;
then r,(x - c1) div m1 are_congruent_mod m2 by Def1;
then (x - c1) div m1,r are_congruent_mod m2 by INT_1:35;
then m2 divides ((x - c1) div m1) - r by INT_2:19;
then consider t being Integer such that
A6: ((x - c1) div m1) - r = m2 * t by INT_1:def 9;
x = c1 + (((x - c1) div m1) * m1) by A5
.= c1 + ((r + (m2 * t)) * m1) by A6
.= (c1 + (r * m1)) + ((m1 * m2) * t) ;
then m1 * m2 divides x - (c1 + (r * m1)) by INT_2:12;
hence x,c1 + (m1 * r) are_congruent_mod m1 * m2 by INT_2:19; :: thesis:

end;

take r ; :: thesis:
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 * m2 ) & ((m1 * r) - (c2 - c1)) mod m2 = 0 ) by A2, A3; :: thesis: