theorem Th21: :: HILB10_1:18

for n being Nat
for a being non trivial Nat
for x being positive Nat holds
( (x |^ n) * ((1 - (1 / ((2 * a) * x))) |^ n) <= (Py ((a * x),(n + 1))) / (Py (a,(n + 1))) & (Py ((a * x),(n + 1))) / (Py (a,(n + 1))) <= (x |^ n) * (1 / ((1 - (1 / (2 * a))) |^ n)) )