theorem Th20: :: HILB10_1:17

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