let a, n be Nat; :: thesis: ( a > 4 & n > 0 implies (a |^ (2 |^ n)) + 1 > 17 )
assume ( a > 4 & n > 0 ) ; :: thesis: (a |^ (2 |^ n)) + 1 > 17
then (a |^ (2 |^ n)) + 1 > 25 by Lm48;
hence (a |^ (2 |^ n)) + 1 > 17 by XXREAL_0:2; :: thesis: verum