let n be Nat; :: thesis: ( n >= 3 implies n ! > n )
assume A1: n >= 3 ; :: thesis: n ! > n
set n1 = n - 1;
2 = 3 - 1 ;
then A2: n - 1 >= 2 by A1, XREAL_1:9;
then reconsider n1 = n - 1 as Element of NAT by INT_1:3;
n1 ! >= 2 by A2, Lm51, NEWTON:14;
then n1 ! > 1 by XXREAL_0:2;
then A3: n * (n1 !) > n * 1 by A1, XREAL_1:68;
n1 + 1 = n ;
hence n ! > n by A3, NEWTON:15; :: thesis: verum