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: denominator p <> 0 by Def3;

A2: now

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 Th37
.= (a / 1) * ((denominator p) / (denominator p))
.= a by A1, XCMPLX_1:60 ;
hence a <= p ; :: thesis: verum

end;

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

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

end;

end;

end;

now

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 Th80; :: thesis: verum

end;

end;

end;

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