let p be Rational; :: thesis: ( p <= - 1 iff numerator p <= - (denominator p) )

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

assume A2: p <= - 1 ; :: thesis: numerator p <= - (denominator p)

per cases ( p = - 1 or p < - 1 ) by A2, XXREAL_0:1;

suppose p = - 1 ; :: thesis: numerator p <= - (denominator p)

hence numerator p <= - (denominator p) ; :: thesis: verum

end;

suppose p < - 1 ; :: thesis: numerator p <= - (denominator p)

hence numerator p <= - (denominator p) by Th28; :: thesis: verum

end;

end;

end;

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

assume A3: numerator p <= - (denominator p) ; :: thesis: p <= - 1

per cases ( numerator p = - (denominator p) or numerator p < - (denominator p) ) by A3, XXREAL_0:1;

suppose numerator p = - (denominator p) ; :: thesis: p <= - 1

hence p <= - 1 by Th21; :: thesis: verum

end;

suppose numerator p < - (denominator p) ; :: thesis: p <= - 1

hence p <= - 1 by Th28; :: thesis: verum

end;

end;

end;

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