let p be Rational; :: thesis: ( p < - 1 iff denominator p < - (numerator p) )
( denominator p < - (numerator p) iff - (- (numerator p)) < - (denominator p) ) by XREAL_1:26;
hence ( p < - 1 iff denominator p < - (numerator p) ) by Th64; :: thesis: verum