let n, k be Nat; :: thesis: (n !) / ((n -' k) !) is Element of NAT
( n in NAT & k in NAT ) by ORDINAL1:def 13;
then (n !) / ((n -' k) !) is integer by IRRAT_1:37, NAT_D:35;
hence (n !) / ((n -' k) !) is Element of NAT by INT_1:16; :: thesis: verum