theorem Th14: :: HILB10_6:14

for n, p being Nat
for a being non trivial Nat st 0 < p |^ n & p |^ n < a holds
(p |^ n) + ((Py (a,n)) * (a - p)) <= Px (a,n)