let p be Rational; :: thesis: ( p <= - 1 iff denominator p <= - (numerator p) )
( denominator p <= - (numerator p) iff - (- (numerator p)) <= - (denominator p) ) by XREAL_1:24;
hence ( p <= - 1 iff denominator p <= - (numerator p) ) by Th29; :: thesis: verum