theorem Th13: :: HILB10_1:10

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