theorem :: NUMBER13:46

for n being non zero Nat st n > 1 holds
(1 / 3) * (((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1) is composite