theorem Th70: :: NUMBER17:70

for a being Nat
for k being Integer st k <> 1 holds
ex n being positive Nat st
( a < (2 |^ (2 |^ n)) + k & (2 |^ (2 |^ n)) + k is composite )