theorem Th3: :: LIOUVIL2:2

for A being positive Real ex n being positive Nat st 1 / (2 |^ n) <= A