theorem :: NUMBER14:29

for a1, a2 being Integer
for n1, n2 being Nat st n1,n2 are_coprime & n1 > 0 & n2 > 0 holds
{ x where x is Nat : x solves_CRT a1,n1,a2,n2 } is infinite