theorem Th14: :: HILB10_1:11

for n, k being Nat
for a being non trivial Nat st k < n holds
Py (a,k) < Py (a,n)