let n be Nat; :: thesis: ( n >= 1 implies (n + 1) ! >= (n !) + 1 )
assume A1: n >= 1 ; :: thesis: (n + 1) ! >= (n !) + 1
n ! >= 1 by Th2;
then n * (n !) >= 1 * 1 by A1, XREAL_1:66;
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