set S = { n where n is Nat : n divides (2 |^ n) + 2 } ;
set X = { n where n is non zero even Nat : ( n divides (2 |^ n) + 2 & n - 1 divides (2 |^ n) + 1 ) } ;
{ n where n is non zero even Nat : ( n divides (2 |^ n) + 2 & n - 1 divides (2 |^ n) + 1 ) } c= { n where n is Nat : n divides (2 |^ n) + 2 }

proof

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

end;

hence { n where n is Nat : n divides (2 |^ n) + 2 } is infinite by Th16; :: thesis: verum