theorem Def2: :: LIOUVIL1:29

for r being Real holds
( r is liouville iff for n being non zero Nat ex p being Integer ex q being Nat st
( 1 < q & 0 < |.(r - (p / q)).| & |.(r - (p / q)).| < 1 / (q |^ n) ) )