theorem Th27: :: NUMBER14:27

for a1, a2 being Integer
for n1, n2 being Nat st n1 > 0 & n2 > 0 holds
for x being Integer st x solves_CRT a1,n1,a2,n2 holds
x mod (n1 * n2) solves_CRT a1,n1,a2,n2