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