theorem Th20: :: HILB10_6:20

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