let n, i be Nat; :: thesis: ( 2 <= i implies i |^ n >= n + 1 )
for n being Nat holds S₁[n] from NAT_1:sch 2(Lm3, Lm4);
hence ( 2 <= i implies i |^ n >= n + 1 ) ; :: thesis: verum