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