defpred S₁[ Nat] means 2 to_power $1 > $1 + 1;
A1: for k being Nat st k >= 2 & S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( k >= 2 & S₁[k] implies S₁[k + 1] )
assume that
k >= 2 and
A2: 2 to_power k > k + 1 ; :: thesis: S₁[k + 1]
2 to_power (k + 1) = (2 to_power k) * (2 to_power 1) by POWER:27
.= (2 to_power k) * 2 by POWER:25
.= (2 to_power k) + (2 to_power k) ;
then A3: 2 to_power (k + 1) > (k + 1) + (2 to_power k) by A2, XREAL_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
2 to_power k >= 0 + 1 by INT_1:7, POWER:34;
then (k + 1) + (2 to_power k) >= (k + 1) + 1 by XREAL_1:6;
hence S₁[k + 1] by A3, XXREAL_0:2; :: thesis: verum

end;

2 to_power 2 = 2 ^2 by POWER:46
.= 4 ;
then A4: S₁[2] ;
for n being Nat st n >= 2 holds
S₁[n] from NAT_1:sch 8(A4, A1);
hence for n being Nat st n >= 2 holds
2 to_power n > n + 1 ; :: thesis: verum