let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume 2 |^ n >= n + 1 ; :: thesis: S₁[n + 1]
then (2 |^ n) - n >= 1 by XREAL_1:19;
then A1: 2 * ((2 |^ n) - n) >= 2 * 1 by XREAL_1:64;
(2 |^ (n + 1)) - ((n + 1) + 1) = (2 * (2 |^ n)) - (((2 * n) - n) + 2) by Th11
.= (2 * ((2 |^ n) - n)) + (n - 2) ;
then (2 |^ (n + 1)) - ((n + 1) + 1) >= 2 + (n - 2) by A1, XREAL_1:6;
then 2 |^ (n + 1) >= 0 + ((n + 1) + 1) by XREAL_1:19;
hence 2 |^ (n + 1) >= (n + 1) + 1 ; :: thesis: verum