let b, c, a be real number ; :: thesis: ( 0 < b & c <= a * b implies c / b <= a )
assume A1: ( b > 0 & a * b >= c ) ; :: thesis: c / b <= a
then (a * b) / b >= c / b by Lm27;
hence c / b <= a by A1, XCMPLX_1:90; :: thesis: verum