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 positive 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 positive Nat : x solves_CRT a1,n1,a2,n2 } is infinite )
assume that
A1: n1,n2 are_coprime and
A2: ( n1 > 0 & n2 > 0 ) ; :: thesis: { x where x is positive 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 } ;
CRT (a1,n1,a2,n2) solves_CRT a1,n1,a2,n2 by A1, A2, Def2;
then (CRT (a1,n1,a2,n2)) + ((1 * n1) * n2) solves_CRT a1,n1,a2,n2 by Th26;
then A3: (CRT (a1,n1,a2,n2)) + (n1 * n2) in { x where x is positive Nat : x solves_CRT a1,n1,a2,n2 } by A2;
A4: { x where x is positive Nat : x solves_CRT a1,n1,a2,n2 } is natural-membered

proof

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

end;

for a being Nat st a in { x where x is positive Nat : x solves_CRT a1,n1,a2,n2 } holds
ex b being Nat st
( b > a & b in { x where x is positive Nat : x solves_CRT a1,n1,a2,n2 } )

proof

let a be Nat; :: thesis: ( a in { x where x is positive Nat : x solves_CRT a1,n1,a2,n2 } implies ex b being Nat st
( b > a & b in { x where x is positive Nat : x solves_CRT a1,n1,a2,n2 } ) )
assume a in { x where x is positive Nat : x solves_CRT a1,n1,a2,n2 } ; :: thesis: ex b being Nat st
( b > a & b in { x where x is positive Nat : x solves_CRT a1,n1,a2,n2 } )
then consider x being positive Nat such that
A5: a = x and
A6: x solves_CRT a1,n1,a2,n2 ;
take b = x + ((1 * n1) * n2); :: thesis: ( b > a & b in { x where x is positive Nat : x solves_CRT a1,n1,a2,n2 } )
x + (n1 * n2) > x + 0 by A2, XREAL_1:8;
hence b > a by A5; :: thesis: b in { x where x is positive Nat : x solves_CRT a1,n1,a2,n2 }
b solves_CRT a1,n1,a2,n2 by A6, Th26;
hence b in { x where x is positive Nat : x solves_CRT a1,n1,a2,n2 } ; :: thesis: verum

end;

hence { x where x is positive Nat : x solves_CRT a1,n1,a2,n2 } is infinite by A3, A4, NUMBER04:1; :: thesis: verum