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

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A2: 2 to_power m >= m ; :: thesis: S₁[m + 1]

per cases ( m = 0 or m > 0 ) ;

suppose A3: m = 0 ; :: thesis: S₁[m + 1]

then 2 to_power (m + 1) = 2 by POWER:25;
hence S₁[m + 1] by A3; :: thesis: verum

end;

suppose A4: m > 0 ; :: thesis: S₁[m + 1]

reconsider m2 = 2 to_power m as Nat ;
( m2 * 2 >= m * 2 & 2 to_power 1 = 2 ) by A2, NAT_1:4, POWER:25;
then A5: 2 to_power (m + 1) >= m * 2 by POWER:27;
m * 2 >= m + 1 by A4, Th1;
hence S₁[m + 1] by A5, XXREAL_0:2; :: thesis: verum

end;

end;

end;

A6: S₁[ 0 ] ;
thus for m being Nat holds S₁[m] from NAT_1:sch 2(A6, A1); :: thesis: verum