theorem Th32: :: RAT_1:35

for p being Rational holds
( p < 1 iff numerator p < denominator p )