let n be Nat; :: thesis: ((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1 >= 7
n + 1 >= 0 + 1 by XREAL_1:6;
then 2 |^ (n + 1) >= 2 |^ 1 by PREPOWER:93;
then A1: 2 |^ (2 |^ (n + 1)) >= 2 |^ 2 by PREPOWER:93;
2 |^ n >= 2 |^ 0 by PREPOWER:93;
then 2 |^ (2 |^ n) >= 2 |^ (2 |^ 0) by PREPOWER:93;
then 2 |^ (2 |^ n) >= 2 |^ 1 by NEWTON:4;
then (2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n)) >= 4 + 2 by A1, Lm2, XREAL_1:7;
then ((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1 >= 6 + 1 by XREAL_1:6;
hence ((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1 >= 7 ; :: thesis: verum