theorem Th10: :: HILB10_6:10

for n, k being Nat st k <= n holds
n ! <= (k !) * (n |^ (n -' k))