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