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

proof

2 |^ 2 = 2 * 2 by NEWTON:81;
hence S₁[2] by NEWTON:14; :: 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 ! < k |^ k ) ; :: thesis: S₁[k + 1]
B2: k >= 1 by B1, XXREAL_0:2;
k + 1 > k + 0 by XREAL_1:6;
then (k + 1) |^ k > k |^ k by B2, PREPOWER:10;
then B3: ((k + 1) |^ k) * (k + 1) > (k |^ k) * (k + 1) by XREAL_1:68;
(k !) * (k + 1) < (k |^ k) * (k + 1) by B1, XREAL_1:68;
then (k !) * (k + 1) < ((k + 1) |^ k) * (k + 1) by B3, XXREAL_0:2;
then (k + 1) ! < ((k + 1) |^ k) * (k + 1) by NEWTON:15;
hence S₁[k + 1] by NEWTON:6; :: 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 ! < b |^ b ) ; :: thesis: verum