let p be Rational; :: thesis:

A1: now :: thesis:

assume A2: p <= 1 ; :: thesis:

per cases by A2, XXREAL_0:1;

suppose p = 1 ; :: thesis:

hence numerator p <= denominator p ; :: thesis:

end;

suppose p < 1 ; :: thesis:

hence numerator p <= denominator p by Th32; :: thesis:

end;

end;

end;

now :: thesis:

assume A3: numerator p <= denominator p ; :: thesis:

per cases by A3, XXREAL_0:1;

suppose numerator p = denominator p ; :: thesis:

hence p <= 1 by Th20; :: thesis:

end;

suppose numerator p < denominator p ; :: thesis:

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

end;

end;

end;

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