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

A3: now :: thesis: ( numerator p < - (denominator p) implies p < - 1 )

assume numerator p < - (denominator p) ; :: thesis: p < - 1
then (numerator p) * ((denominator p) ") < ((- 1) * (denominator p)) * ((denominator p) ") by A2, XREAL_1:68;
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 Th12; :: thesis: verum

end;

A4: 0 < denominator p by Th7;

now :: thesis: ( p < - 1 implies numerator p < - (denominator p) )

assume p < - 1 ; :: thesis: numerator p < - (denominator p)
then (numerator p) / (denominator p) < - 1 by Th12;
then ((numerator p) / (denominator p)) * (denominator p) < (- 1) * (denominator p) by A4, XREAL_1:68;
hence numerator p < - (denominator p) by A1, XCMPLX_1:87; :: thesis: verum

end;

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