theorem :: RAT_1:40

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