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