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 Th28; :: thesis: verum