let a be Real; :: thesis: for p being Rational holds
( a < p iff a * (denominator p) < numerator p )
let p be Rational; :: thesis: ( a < p iff a * (denominator p) < numerator p )
A1: 0 < (denominator p) " by Th9;
A2: 0 <> denominator p by Def3;

A3: now :: thesis: ( a * (denominator p) < numerator p implies a < p )

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

end;

0 < denominator p by Th7;
hence ( a < p iff a * (denominator p) < numerator p ) by A3, XREAL_1:68; :: thesis: verum