let n be positive Nat; :: thesis: (2 * (2 |^ (2 |^ n))) + 1 is composite
H₁(2,n) >= (2 * 2) + 1 by Lm15;
hence H₁(2,n) >= 2 by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (2 * (2 |^ (2 |^ n))) + 1 is prime
(2 * (2 |^ (2 |^ n))) + 1 <> 3 ;
hence not (2 * (2 |^ (2 |^ n))) + 1 is prime by Lm13; :: thesis: verum