let k be Integer; :: thesis: ( k <> 1 implies not { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } is empty )
set X = { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } ;
assume k <> 1 ; :: thesis: not { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } is empty
then consider n being positive Nat such that
1 < (2 |^ (2 |^ n)) + k and
A1: (2 |^ (2 |^ n)) + k is composite by Th70;
(2 |^ (2 |^ n)) + k in { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } by A1;
hence not { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } is empty ; :: thesis: verum