theorem :: NUMBER09:49
for a being Nat st 1 < a & a <= 100 holds
ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )