theorem Th13: :: HILB10_4:13

for n, k being Nat st k <= n holds
n choose k <= n |^ k