theorem :: NUMBER05:20

for n being Nat holds (2 |^ (2 |^ n)) + 1 divides (2 |^ ((2 |^ (2 |^ n)) + 1)) - 2