defpred S₁[ Nat] means for n being Nat st n <= $1 holds
n ! <= $1 ! ;
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: for n being Nat st n <= k holds
n ! <= k ! ; :: thesis: S₁[k + 1]
let n be Nat; :: thesis: ( n <= k + 1 implies n ! <= (k + 1) ! )
assume A3: n <= k + 1 ; :: thesis: n ! <= (k + 1) !

per cases ( n <= k or n = k + 1 ) by A3, NAT_1:8;

suppose A4: n <= k ; :: thesis: n ! <= (k + 1) !

k + 1 >= 0 + 1 by XREAL_1:6;
then (k + 1) * (k !) >= 1 * (k !) by XREAL_1:64;
then A5: (k + 1) ! >= k ! by NEWTON:15;
n ! <= k ! by A2, A4;
hence n ! <= (k + 1) ! by A5, XXREAL_0:2; :: thesis: verum

end;

suppose n = k + 1 ; :: thesis: n ! <= (k + 1) !

hence n ! <= (k + 1) ! ; :: thesis: verum

end;

end;

end;

A6: S₁[ 0 ] ;
for n1 being Nat holds S₁[n1] from NAT_1:sch 2(A6, A1);
hence for n1, n being Nat st n <= n1 holds
n ! <= n1 ! ; :: thesis: verum