theorem Th40: :: INT_4:40

for m1, m2, c1, c2 being Integer st m1 <> 0 & m2 <> 0 & m1,m2 are_coprime holds
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 * m2 ) & ((m1 * r) - (c2 - c1)) mod m2 = 0 )