let n be Nat; :: thesis: 2 |^ (2 |^ n) > 1
defpred S₁[ Nat] means 2 |^ (2 |^ $1) > 1;
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: 2 |^ (2 |^ k) > 1 ; :: thesis: S₁[k + 1]
then 2 |^ (2 |^ k) < (2 |^ (2 |^ k)) |^ 2 by PREPOWER:13;
then ( 2 |^ (k + 1) = (2 |^ k) * 2 & 1 < (2 |^ (2 |^ k)) |^ 2 ) by A2, NEWTON:6, XXREAL_0:2;
hence S₁[k + 1] by NEWTON:9; :: thesis: verum

end;

2 |^ 0 = 1 by NEWTON:4;
then 2 |^ (2 |^ 0) = 2 ;
then A3: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A1);
hence 2 |^ (2 |^ n) > 1 ; :: thesis: verum