theorem Th8: :: HILB10_6:8

for n, k being Nat st n >= k holds
n choose k <= (n |^ k) / (k !)