let b be Nat; :: thesis: ( b >= 2 implies b ! < b |^ b )
defpred S1[ Nat] means $1 ! < $1 |^ $1;
A1: S1[2]
proof
2 |^ 2 = 2 * 2 by NEWTON:81;
hence S1[2] by NEWTON:14; :: thesis: verum
end;
A2: for k being Nat st k >= 2 & S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( k >= 2 & S1[k] implies S1[k + 1] )
assume B1: ( k >= 2 & k ! < k |^ k ) ; :: thesis: S1[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 S1[k + 1] by NEWTON:6; :: thesis: verum
end;
for x being Nat st x >= 2 holds
S1[x] from NAT_1:sch 8(A1, A2);
 hence ( b >= 2 implies b ! < b |^ b ) ; :: thesis: verum