theorem :: RAT_1:36

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