set X = { n where n is non zero even Nat : ( n divides (2 |^ n) + 2 & n - 1 divides (2 |^ n) + 1 ) } ;
A1: 2 = 2 * 1 ;
(2 |^ 2) + 2 = 2 * 3 by Lm2;
then A2: 2 divides (2 |^ 2) + 2 ;
2 - 1 divides (2 |^ 2) + 1 by INT_2:12;
then A3: 2 in { n where n is non zero even Nat : ( n divides (2 |^ n) + 2 & n - 1 divides (2 |^ n) + 1 ) } by A1, A2;
A4: { n where n is non zero even Nat : ( n divides (2 |^ n) + 2 & n - 1 divides (2 |^ n) + 1 ) } is natural-membered

proof

let x be object ; :: according to MEMBERED:def 6 :: thesis: ( not x in { n where n is non zero even Nat : ( n divides (2 |^ n) + 2 & n - 1 divides (2 |^ n) + 1 ) } or not x is natural )
assume x in { n where n is non zero even Nat : ( n divides (2 |^ n) + 2 & n - 1 divides (2 |^ n) + 1 ) } ; :: thesis: x is natural
then ex n being non zero even Nat st
( x = n & n divides (2 |^ n) + 2 & n - 1 divides (2 |^ n) + 1 ) ;
hence x is natural ; :: thesis: verum

end;

for a being Nat st a in { n where n is non zero even Nat : ( n divides (2 |^ n) + 2 & n - 1 divides (2 |^ n) + 1 ) } holds
ex b being Nat st
( b > a & b in { n where n is non zero even Nat : ( n divides (2 |^ n) + 2 & n - 1 divides (2 |^ n) + 1 ) } )

proof

let a be Nat; :: thesis: ( a in { n where n is non zero even Nat : ( n divides (2 |^ n) + 2 & n - 1 divides (2 |^ n) + 1 ) } implies ex b being Nat st
( b > a & b in { n where n is non zero even Nat : ( n divides (2 |^ n) + 2 & n - 1 divides (2 |^ n) + 1 ) } ) )
assume a in { n where n is non zero even Nat : ( n divides (2 |^ n) + 2 & n - 1 divides (2 |^ n) + 1 ) } ; :: thesis: ex b being Nat st
( b > a & b in { n where n is non zero even Nat : ( n divides (2 |^ n) + 2 & n - 1 divides (2 |^ n) + 1 ) } )
then consider n being non zero even Nat such that
A5: a = n and
A6: ( n divides (2 |^ n) + 2 & n - 1 divides (2 |^ n) + 1 ) ;
take b = (2 |^ n) + 2; :: thesis: ( b > a & b in { n where n is non zero even Nat : ( n divides (2 |^ n) + 2 & n - 1 divides (2 |^ n) + 1 ) } )
A7: n < 2 |^ n by NEWTON:86;
2 |^ n <= (2 |^ n) + 2 by NAT_1:11;
hence b > a by A5, A7, XXREAL_0:2; :: thesis: b in { n where n is non zero even Nat : ( n divides (2 |^ n) + 2 & n - 1 divides (2 |^ n) + 1 ) }
( b - 1 divides (2 |^ b) + 1 & b divides (2 |^ b) + 2 ) by A6, Th15;
hence b in { n where n is non zero even Nat : ( n divides (2 |^ n) + 2 & n - 1 divides (2 |^ n) + 1 ) } ; :: thesis: verum

end;

hence { n where n is non zero even Nat : ( n divides (2 |^ n) + 2 & n - 1 divides (2 |^ n) + 1 ) } is infinite by A3, A4, Th1; :: thesis: verum