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