consider crt being Nat such that
A1: 6700417 < crt and
A2: for n being Nat holds
( crt < 2 * ((2 |^ 64) - 1) & crt + ((n * 2) * ((2 |^ 64) - 1)),1 are_congruent_mod ((2 |^ 32) - 1) * 641 & crt + ((n * 2) * ((2 |^ 64) - 1)), - 1 are_congruent_mod 6700417 & crt + ((n * 2) * ((2 |^ 64) - 1)),1 are_congruent_mod 2 ) by Th31;
defpred S₁[ Nat] means for n being positive Nat holds (2 |^ n) + $1 is composite ;
set I = { (crt + ((k * 2) * ((2 |^ 64) - 1))) where k is Nat : S₁[crt + ((k * 2) * ((2 |^ 64) - 1))] } ;
(((2 |^ 32) - 1) * 641) * 6700417 = ((2 |^ 32) - 1) * (641 * 6700417)
.= ((2 |^ 32) - 1) * ((2 |^ 32) + 1) by Th28
.= ((2 |^ 32) * (2 |^ 32)) - (1 * 1)
.= (2 |^ (32 + 32)) - 1 by NEWTON:8 ;
then (2 |^ 64) - 1 >= 6700417 * 1 by NAT_1:14, XREAL_1:64;
then ( 2 * ((2 |^ 64) - 1) >= 6700417 * 2 & 6700417 * 2 > 6700417 * 1 ) by XREAL_1:64;
then A3: 2 * ((2 |^ 64) - 1) > 6700417 * 1 by XXREAL_0:2;
( crt + ((0 * 2) * ((2 |^ 64) - 1)),1 are_congruent_mod ((2 |^ 32) - 1) * 641 & crt + ((0 * 2) * ((2 |^ 64) - 1)), - 1 are_congruent_mod 6700417 ) by A2;
then S₁[crt + ((0 * 2) * ((2 |^ 64) - 1))] by Th35, A1;
then A4: crt + ((0 * 2) * ((2 |^ 64) - 1)) in { (crt + ((k * 2) * ((2 |^ 64) - 1))) where k is Nat : S₁[crt + ((k * 2) * ((2 |^ 64) - 1))] } ;

now :: thesis: for x being object st x in { (crt + ((k * 2) * ((2 |^ 64) - 1))) where k is Nat : S₁[crt + ((k * 2) * ((2 |^ 64) - 1))] } holds
x is natural

let x be object ; :: thesis: ( x in { (crt + ((k * 2) * ((2 |^ 64) - 1))) where k is Nat : S₁[crt + ((k * 2) * ((2 |^ 64) - 1))] } implies x is natural )
assume x in { (crt + ((k * 2) * ((2 |^ 64) - 1))) where k is Nat : S₁[crt + ((k * 2) * ((2 |^ 64) - 1))] } ; :: thesis: x is natural
then ex k being Nat st
( x = crt + ((k * 2) * ((2 |^ 64) - 1)) & S₁[crt + ((k * 2) * ((2 |^ 64) - 1))] ) ;
hence x is natural ; :: thesis: verum

end;

then A5: { (crt + ((k * 2) * ((2 |^ 64) - 1))) where k is Nat : S₁[crt + ((k * 2) * ((2 |^ 64) - 1))] } is non empty natural-membered set by A4, MEMBERED:def 6;
A6: for a being Nat st a in { (crt + ((k * 2) * ((2 |^ 64) - 1))) where k is Nat : S₁[crt + ((k * 2) * ((2 |^ 64) - 1))] } holds
ex b being Nat st
( b > a & b in { (crt + ((k * 2) * ((2 |^ 64) - 1))) where k is Nat : S₁[crt + ((k * 2) * ((2 |^ 64) - 1))] } )

proof

let a be Nat; :: thesis: ( a in { (crt + ((k * 2) * ((2 |^ 64) - 1))) where k is Nat : S₁[crt + ((k * 2) * ((2 |^ 64) - 1))] } implies ex b being Nat st
( b > a & b in { (crt + ((k * 2) * ((2 |^ 64) - 1))) where k is Nat : S₁[crt + ((k * 2) * ((2 |^ 64) - 1))] } ) )
assume a in { (crt + ((k * 2) * ((2 |^ 64) - 1))) where k is Nat : S₁[crt + ((k * 2) * ((2 |^ 64) - 1))] } ; :: thesis: ex b being Nat st
( b > a & b in { (crt + ((k * 2) * ((2 |^ 64) - 1))) where k is Nat : S₁[crt + ((k * 2) * ((2 |^ 64) - 1))] } )
then consider k being Nat such that
A7: ( a = crt + ((k * 2) * ((2 |^ 64) - 1)) & S₁[crt + ((k * 2) * ((2 |^ 64) - 1))] ) ;
A8: ( crt + (((k + 1) * 2) * ((2 |^ 64) - 1)) = a + (2 * ((2 |^ 64) - 1)) & a + (2 * ((2 |^ 64) - 1)) > 0 + 6700417 & a + (2 * ((2 |^ 64) - 1)) > a + 0 ) by A7, A3, XREAL_1:8;
( crt + (((k + 1) * 2) * ((2 |^ 64) - 1)),1 are_congruent_mod ((2 |^ 32) - 1) * 641 & crt + (((k + 1) * 2) * ((2 |^ 64) - 1)), - 1 are_congruent_mod 6700417 ) by A2;
then S₁[crt + (((k + 1) * 2) * ((2 |^ 64) - 1))] by A8, Th35;
then crt + (((k + 1) * 2) * ((2 |^ 64) - 1)) in { (crt + ((k * 2) * ((2 |^ 64) - 1))) where k is Nat : S₁[crt + ((k * 2) * ((2 |^ 64) - 1))] } ;
hence ex b being Nat st
( b > a & b in { (crt + ((k * 2) * ((2 |^ 64) - 1))) where k is Nat : S₁[crt + ((k * 2) * ((2 |^ 64) - 1))] } ) by A8; :: thesis: verum

end;

{ (crt + ((k * 2) * ((2 |^ 64) - 1))) where k is Nat : S₁[crt + ((k * 2) * ((2 |^ 64) - 1))] } c= { k where k is Nat : S₁[k] }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (crt + ((k * 2) * ((2 |^ 64) - 1))) where k is Nat : S₁[crt + ((k * 2) * ((2 |^ 64) - 1))] } or x in { k where k is Nat : S₁[k] } )
assume x in { (crt + ((k * 2) * ((2 |^ 64) - 1))) where k is Nat : S₁[crt + ((k * 2) * ((2 |^ 64) - 1))] } ; :: thesis: x in { k where k is Nat : S₁[k] }
then ex k being Nat st
( x = crt + ((k * 2) * ((2 |^ 64) - 1)) & S₁[crt + ((k * 2) * ((2 |^ 64) - 1))] ) ;
hence x in { k where k is Nat : S₁[k] } ; :: thesis: verum

end;

hence { k where k is Nat : for n being positive Nat holds (2 |^ n) + k is composite } is infinite by A6, A5, NUMBER04:1; :: thesis: verum