theorem Th17: :: HILB10_1:14

for n, k being Nat
for a being non trivial Nat st a <> 2 & k <= n holds
2 * (Py (a,k)) < Px (a,n)