let s be positive Nat; :: thesis: 2 |^ (2 |^ ((2 * s) + 1)) >= 256
2 * s >= 2 * 1 by NAT_1:14, XREAL_1:64;
then (2 * s) + 1 >= 2 + 1 by XREAL_1:6;
then 2 |^ ((2 * s) + 1) >= 2 |^ 3 by PREPOWER:93;
hence 2 |^ (2 |^ ((2 * s) + 1)) >= 256 by Lm6, Lm2, PREPOWER:93; :: thesis: verum