let n be Nat; :: thesis: ( n >= 1 implies 2 <= (n + 1) ! )
assume n >= 1 ; :: thesis: 2 <= (n + 1) !
then n + 1 >= 1 + 1 by XREAL_1:7;
then 1 < (n + 1) ! by ASYMPT_1:55;
then 1 + 1 <= (n + 1) ! by NAT_1:13;
hence 2 <= (n + 1) ! ; :: thesis: verum