theorem Th7: :: HILB10_6:7

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