let s be positive Nat; :: thesis: (2 |^ (2 |^ ((2 * s) + 1))) + 3 is composite
set m = (2 |^ (2 |^ ((2 * s) + 1))) + 3;
A1: (2 |^ (2 |^ ((2 * s) + 1))) + 3 >= 256 + 3 by Lm14, XREAL_1:6;
hence (2 |^ (2 |^ ((2 * s) + 1))) + 3 >= 2 by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (2 |^ (2 |^ ((2 * s) + 1))) + 3 is prime
(2 |^ (2 |^ ((2 * s) + 1))) + 3 <> 7 by A1;
hence not (2 |^ (2 |^ ((2 * s) + 1))) + 3 is prime by Th74; :: thesis: verum