:: deftheorem defines liouville LIOUVIL1:def 5 :
for x being Real holds
( x is liouville iff for n being Nat ex p being Integer ex q being Nat st
( q > 1 & 0 < |.(x - (p / q)).| & |.(x - (p / q)).| < 1 / (q |^ n) ) );