let n, k be Nat; :: thesis: (n !) / ((n -' k) !) is Element of NAT
(n !) / ((n -' k) !) is integer by IRRAT_1:36, NAT_D:35;
hence (n !) / ((n -' k) !) is Element of NAT by INT_1:3; :: thesis: verum