theorem :: ASYMPT_1:56

for n1, n being Nat st n <= n1 holds
n ! <= n1 ! by Lm51;