defpred S1[ Nat] means 2 to_power $1 >= $1;
A1: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume A2: 2 to_power m >= m ; :: thesis: S1[m + 1]
per cases ( m = 0 or m > 0 ) ;
suppose A3: m = 0 ; :: thesis: S1[m + 1]
then 2 to_power (m + 1) = 2 by POWER:25;
hence S1[m + 1] by A3; :: thesis: verum
end;
suppose A4: m > 0 ; :: thesis: S1[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 S1[m + 1] by A5, XXREAL_0:2; :: thesis: verum
end;
end;
end;
A6: S1[ 0 ] ;
thus for m being Nat holds S1[m] from NAT_1:sch 2(A6, A1); :: thesis: verum