for a being Real
for p being Rational holds
( a <= p iff a * (denominator p) <= numerator p )