theorem Th28: :: LIOUVIL2:27

for f being INT -valued non-zero Polynomial of F_Real
for a being irrational Element of F_Real st a is_a_root_of f holds
ex A being positive Real st
for p being Integer
for q being positive Nat holds |.(a - (p / q)).| > A / (q |^ (len f))