theorem Th19: :: HILB10_6:19

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