set X = { ((10 |^ n) + 3) where n is Nat : (10 |^ n) + 3 is composite } ;
set z = (10 |^ ((6 * 0) + 4)) + 3;
(10 |^ ((6 * 0) + 4)) + 3 is composite by Th66;
then A1: (10 |^ ((6 * 0) + 4)) + 3 in { ((10 |^ n) + 3) where n is Nat : (10 |^ n) + 3 is composite } ;
A2: { ((10 |^ n) + 3) where n is Nat : (10 |^ n) + 3 is composite } is natural-membered

proof

let x be object ; :: according to MEMBERED:def 6 :: thesis: ( not x in { ((10 |^ n) + 3) where n is Nat : (10 |^ n) + 3 is composite } or not x is natural )
assume x in { ((10 |^ n) + 3) where n is Nat : (10 |^ n) + 3 is composite } ; :: thesis: x is natural
then ex n being Nat st
( x = (10 |^ n) + 3 & (10 |^ n) + 3 is composite ) ;
hence x is natural ; :: thesis: verum

end;

for a being Nat st a in { ((10 |^ n) + 3) where n is Nat : (10 |^ n) + 3 is composite } holds
ex b being Nat st
( b > a & b in { ((10 |^ n) + 3) where n is Nat : (10 |^ n) + 3 is composite } )

proof

let a be Nat; :: thesis: ( a in { ((10 |^ n) + 3) where n is Nat : (10 |^ n) + 3 is composite } implies ex b being Nat st
( b > a & b in { ((10 |^ n) + 3) where n is Nat : (10 |^ n) + 3 is composite } ) )
assume a in { ((10 |^ n) + 3) where n is Nat : (10 |^ n) + 3 is composite } ; :: thesis: ex b being Nat st
( b > a & b in { ((10 |^ n) + 3) where n is Nat : (10 |^ n) + 3 is composite } )
then consider n being Nat such that
A3: a = (10 |^ n) + 3 and
(10 |^ n) + 3 is composite ;
take b = (10 |^ ((6 * (n + 1)) + 4)) + 3; :: thesis: ( b > a & b in { ((10 |^ n) + 3) where n is Nat : (10 |^ n) + 3 is composite } )
n + 0 < n + 1 by XREAL_1:8;
then 1 * n < 6 * (n + 1) by XREAL_1:96;
then n + 0 < (6 * (n + 1)) + 4 by XREAL_1:8;
then 10 |^ n < 10 |^ ((6 * (n + 1)) + 4) by PEPIN:66;
hence b > a by A3, XREAL_1:8; :: thesis: b in { ((10 |^ n) + 3) where n is Nat : (10 |^ n) + 3 is composite }
b is composite by Th66;
hence b in { ((10 |^ n) + 3) where n is Nat : (10 |^ n) + 3 is composite } ; :: thesis: verum

end;

hence { ((10 |^ n) + 3) where n is Nat : (10 |^ n) + 3 is composite } is infinite by A1, A2, Th1; :: thesis: verum