theorem Th19: :: HILB10_1:16

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