let n, k be Element of NAT ; :: thesis: (n ! ) / ((n -' k) ! ) is Element of NAT
(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