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

end;

suppose numerator p < denominator p ; :: thesis: p <= 1

hence p <= 1 by Th32; :: thesis: verum

end;

end;

end;

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