theorem Th29: :: RAT_1:32

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