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