let b be Nat; :: thesis: ( b >= 2 implies (b + 1) ! > 2 |^ b )
defpred S₁[ Nat] means ($1 + 1) ! > 2 |^ $1;
A1: S₁[2]

proof

B1: (2 + 1) ! = 2 * 3 by NEWTON:14, NEWTON:15;
2 |^ 2 = 2 * 2 by NEWTON:81;
hence S₁[2] by B1; :: thesis: verum

end;

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

proof

let k be Nat; :: thesis: ( k >= 2 & S₁[k] implies S₁[k + 1] )
assume B1: ( k >= 2 & (k + 1) ! > 2 |^ k ) ; :: thesis: S₁[k + 1]
then k + 2 > 2 + 0 by XREAL_1:6;
then ((k + 1) !) * ((k + 1) + 1) > (2 |^ k) * 2 by B1, XREAL_1:96;
then ((k + 1) !) * ((k + 1) + 1) > 2 |^ (k + 1) by NEWTON:6;
hence S₁[k + 1] by NEWTON:15; :: thesis: verum

end;

for x being Nat st x >= 2 holds
S₁[x] from NAT_1:sch 8(A1, A2);
hence ( b >= 2 implies (b + 1) ! > 2 |^ b ) ; :: thesis: verum