theorem Th39: :: NUMBER13:39
for n being Nat holds ((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1 >= 7