theorem :: NUMBER17:75
for s being positive Nat holds (2 |^ (2 |^ ((2 * s) + 1))) + 3 is composite