theorem :: NUMBER17:79
for s being positive Nat holds (2 |^ (2 |^ ((6 * s) + 2))) + 13 is composite