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 )

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

assume A3: a * (denominator p) <= numerator p ; :: thesis: a <= p

per cases ( a * (denominator p) = numerator p or a * (denominator p) < numerator p ) by A3, XXREAL_0:1;

suppose a * (denominator p) = numerator p ; :: thesis: a <= p

then p = (a * (denominator p)) / (1 * (denominator p)) by Th12
.= (a / 1) * ((denominator p) / (denominator p))
.= a by XCMPLX_1:60 ;
hence a <= p ; :: thesis: verum

end;

suppose a * (denominator p) < numerator p ; :: thesis: a <= p

hence a <= p by Th36; :: thesis: verum

end;

end;

end;

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

assume A4: a <= p ; :: thesis: numerator p >= a * (denominator p)

per cases ( a = p or a < p ) by A4, XXREAL_0:1;

suppose a = p ; :: thesis: numerator p >= a * (denominator p)

hence numerator p >= a * (denominator p) ; :: thesis: verum

end;

suppose a < p ; :: thesis: a * (denominator p) <= numerator p

hence a * (denominator p) <= numerator p by Th36; :: thesis: verum

end;

end;

end;

hence ( a <= p iff a * (denominator p) <= numerator p ) by A2; :: thesis: verum