let n, k be Element of NAT ; :: thesis: (n ! ) / (k ! ) > 0
( n ! > 0 & k ! > 0 ) by NEWTON:23;
hence (n ! ) / (k ! ) > 0 by XREAL_1:141; :: thesis: verum