for a being Real
for t being 1 _greater Nat ex x, y being Integer st
( |.((x * a) - y).| < 1 / t & 0 < x & x <= t )