theorem Th18: :: HILB10_1:15

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