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 )

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 XREAL_1:68;
then a * ((denominator p) * ((denominator p) ")) < (numerator p) * ((denominator p) ") ;
then a * 1 < (numerator p) * ((denominator p) ") by XCMPLX_0:def 7;
hence a < p by Th12; :: thesis: verum

end;

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