theorem Th36: :: RAT_1:39

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