for a, b, c being Integer
for n1, n2, n3 being non zero Nat st n1 gcd n2 divides a - b holds
ex r, s being Integer st
for x being Integer st (x - a) mod n1 = 0 & (x - b) mod n2 = 0 & (x - c) mod n3 = 0 holds
( x,(a + (n1 * r)) + ((n1 lcm n2) * s) are_congruent_mod (n1 lcm n2) lcm n3 & (((n1 div (n1 gcd n2)) * r) - ((b - a) div (n1 gcd n2))) mod (n2 div (n1 gcd n2)) = 0 & ((((n1 lcm n2) div ((n1 lcm n2) gcd n3)) * s) - ((c - (a + (n1 * r))) div ((n1 lcm n2) gcd n3))) mod (n3 div ((n1 lcm n2) gcd n3)) = 0 )