for n, k being Element of NAT st k >= 1 & n ! <= k & k < (n + 1) ! holds
Step1 k = n ! by Def6;