for a being NAT -valued Real_Sequence
for b being non trivial Nat st rng a c= b & a is eventually-non-zero holds
for n being non zero Nat ex p being Integer ex q being Nat st
( q > 1 & 0 < |.((Liouville_constant (a,b)) - (p / q)).| & |.((Liouville_constant (a,b)) - (p / q)).| < 1 / (q |^ n) )