let a, n be Nat; :: thesis: ( 1 <= a implies (2 |^ (2 |^ n)) + ((6 * a) - 1) > 6 )

assume 1 <= a ; :: thesis: (2 |^ (2 |^ n)) + ((6 * a) - 1) > 6

then 6 * 1 <= 6 * a by XREAL_1:64;

then A1: (6 * 1) - 1 <= (6 * a) - 1 by XREAL_1:9;

0 + 1 <= 2 |^ n by NAT_1:13;

then 2 <= 2 |^ (2 |^ n) by PREPOWER:12;

then 2 + 5 <= (2 |^ (2 |^ n)) + ((6 * a) - 1) by A1, XREAL_1:7;

hence (2 |^ (2 |^ n)) + ((6 * a) - 1) > 6 by XXREAL_0:2; :: thesis: verum

assume 1 <= a ; :: thesis: (2 |^ (2 |^ n)) + ((6 * a) - 1) > 6

then 6 * 1 <= 6 * a by XREAL_1:64;

then A1: (6 * 1) - 1 <= (6 * a) - 1 by XREAL_1:9;

0 + 1 <= 2 |^ n by NAT_1:13;

then 2 <= 2 |^ (2 |^ n) by PREPOWER:12;

then 2 + 5 <= (2 |^ (2 |^ n)) + ((6 * a) - 1) by A1, XREAL_1:7;

hence (2 |^ (2 |^ n)) + ((6 * a) - 1) > 6 by XXREAL_0:2; :: thesis: verum