let s be positive Nat; :: thesis: 2 |^ (2 |^ ((4 * s) + 1)) >= 2 |^ 32
4 * s >= 4 * 1 by NAT_1:14, XREAL_1:64;
then (4 * s) + 1 >= 4 + 1 by XREAL_1:6;
then 2 |^ ((4 * s) + 1) >= 2 |^ 5 by PREPOWER:93;
hence 2 |^ (2 |^ ((4 * s) + 1)) >= 2 |^ 32 by Lm4, PREPOWER:93; :: thesis: verum