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 Lm32;
hence c / b < a by A1, XCMPLX_1:90; :: thesis: verum