let p be Rational; :: thesis: ( p < - 1 iff numerator p < - (denominator p) )
A1: 0 <> denominator p by Def3;
A2: 0 < (denominator p) " by Th30;

A3: now

assume numerator p < - (denominator p) ; :: thesis: p < - 1
then (numerator p) * ((denominator p) " ) < ((- 1) * (denominator p)) * ((denominator p) " ) by A2, XREAL_1:70;
then (numerator p) * ((denominator p) " ) < (- 1) * ((denominator p) * ((denominator p) " )) ;
then (numerator p) * ((denominator p) " ) < (- 1) * 1 by A1, XCMPLX_0:def 7;
hence p < - 1 by Th37; :: thesis: verum

end;

A4: 0 < denominator p by Th27;

now

assume p < - 1 ; :: thesis: numerator p < - (denominator p)
then (numerator p) / (denominator p) < - 1 by Th37;
then ((numerator p) / (denominator p)) * (denominator p) < (- 1) * (denominator p) by A4, XREAL_1:70;
hence numerator p < - (denominator p) by A1, XCMPLX_1:88; :: thesis: verum

end;

hence ( p < - 1 iff numerator p < - (denominator p) ) by A3; :: thesis: verum