let n be Nat; :: thesis: ( n >= 2 implies (n + 1) ! > (n !) + 1 )
assume n >= 2 ; :: thesis: (n + 1) ! > (n !) + 1
then n >= 1 + 1 ;
then A1: n > 1 by NAT_1:13;
n ! >= n by NEWTON:38;
then n ! > 1 by A1, XXREAL_0:2;
then n * (n !) > 1 * 1 by A1, XREAL_1:96;
then ((n + 1) !) - (n !) > 1 by Th3;
then (((n + 1) !) - (n !)) + (n !) > 1 + (n !) by XREAL_1:6;
hence (n + 1) ! > (n !) + 1 ; :: thesis: verum