defpred S₁[ Nat] means $1 ! > 1;
A1: 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 that
A2: k >= 2 and
A3: k ! > 1 ; :: thesis: S₁[k + 1]
A4: k + 1 > 0 + 1 by A2, XREAL_1:6;
(k + 1) * (k !) > (k + 1) * 1 by A3, XREAL_1:68;
then (k + 1) * (k !) > 1 by A4, XXREAL_0:2;
hence S₁[k + 1] by NEWTON:15; :: thesis: verum

end;

A5: S₁[2] by NEWTON:14;
for n being Nat st n >= 2 holds
S₁[n] from NAT_1:sch 8(A5, A1);
hence for n being Nat st n >= 2 holds
n ! > 1 ; :: thesis: verum