defpred S₁[ Nat] means 2 to_power $1 > $1 to_power 6;
A1: S₁[30]

proof

2 to_power 30 = 2 to_power (5 * 6)
.= 32 to_power 6 by Lm10, POWER:38 ;
hence S₁[30] by POWER:42; :: thesis: verum

end;

A2: for n being Nat st n >= 30 & S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( n >= 30 & S₁[n] implies S₁[n + 1] )
assume that
A3: n >= 30 and
A4: 2 to_power n > n to_power 6 ; :: thesis: S₁[n + 1]
A5: 2 to_power (n + 1) = (2 to_power n) * (2 to_power 1) by POWER:32
.= (2 to_power n) * 2 by POWER:30 ;
A6: (2 to_power n) * 2 > (n to_power 6) * 2 by A4, XREAL_1:70;
n >= 9 by A3, XXREAL_0:2;
then (n + 1) to_power 6 < 2 * (n to_power 6) by Lm35;
hence S₁[n + 1] by A5, A6, XXREAL_0:2; :: thesis: verum

end;

for n being Nat st n >= 30 holds
S₁[n] from NAT_1:sch 8(A1, A2);
hence for n being Element of NAT st n >= 30 holds
2 to_power n > n to_power 6 ; :: thesis: verum