theorem Th2: :: LIOUVIL2:1

for m being Nat st 2 <= m holds
for A being Real ex n being positive Nat st A <= m |^ n