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

end;

for n being Nat st n >= 2 holds
S₁[n] from NAT_1:sch 8(A1, A2);
hence for n being Element of NAT st n >= 2 holds
n ! > 1 ; :: thesis: verum