for a, n being Nat st 1 <= a holds
(2 |^ (2 |^ n)) + ((6 * a) - 1) > 6