let a be real number ; :: 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 Th30;
A2: 0 <> denominator p by Def3;

A3: now

assume a * (denominator p) < numerator p ; :: thesis: a < p
then (a * (denominator p)) * ((denominator p) " ) < (numerator p) * ((denominator p) " ) by A1, XREAL_1:70;
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 Th37; :: thesis: verum

end;

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