let a1, a2 be Integer; :: thesis: 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
let n1, n2 be Nat; :: thesis: ( n1,n2 are_coprime & n1 > 0 & n2 > 0 implies { x where x is Nat : x solves_CRT a1,n1,a2,n2 } is infinite )
set X = { x where x is positive Nat : x solves_CRT a1,n1,a2,n2 } ;
{ x where x is positive Nat : x solves_CRT a1,n1,a2,n2 } c= { x where x is Nat : x solves_CRT a1,n1,a2,n2 }

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { x where x is positive Nat : x solves_CRT a1,n1,a2,n2 } or e in { x where x is Nat : x solves_CRT a1,n1,a2,n2 } )
assume e in { x where x is positive Nat : x solves_CRT a1,n1,a2,n2 } ; :: thesis: e in { x where x is Nat : x solves_CRT a1,n1,a2,n2 }
then ex x being positive Nat st
( e = x & x solves_CRT a1,n1,a2,n2 ) ;
hence e in { x where x is Nat : x solves_CRT a1,n1,a2,n2 } ; :: thesis: verum

end;

hence ( n1,n2 are_coprime & n1 > 0 & n2 > 0 implies { x where x is Nat : x solves_CRT a1,n1,a2,n2 } is infinite ) by Th28; :: thesis: verum