let s be positive Nat; :: thesis: 2 |^ (2 |^ ((10 * s) + 1)) >= 2 |^ 2048
10 * s >= 10 * 1 by NAT_1:14, XREAL_1:64;
then (10 * s) + 1 >= 10 + 1 by XREAL_1:6;
then 2 |^ ((10 * s) + 1) >= 2 |^ 11 by PREPOWER:93;
hence 2 |^ (2 |^ ((10 * s) + 1)) >= 2 |^ 2048 by Lm8, PREPOWER:93; :: thesis: verum