theorem :: RAT_1:33

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