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