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

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

assume numerator p < denominator p ; :: thesis: p < 1
then (numerator p) * ((denominator p) ") < (denominator p) * ((denominator p) ") by XREAL_1:68;
then (numerator p) * ((denominator p) ") < 1 by XCMPLX_0:def 7;
hence p < 1 by Th12; :: thesis: verum

end;

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 XREAL_1:68;
hence numerator p < denominator p by XCMPLX_1:87; :: thesis: verum

end;

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