theorem Th28: :: RAT_1:31

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