let c, b, a be real number ; :: thesis: ( 0 <= c & b < 0 & a <= b implies c / b <= c / a )
assume A1: ( c >= 0 & b < 0 & a <= b ) ; :: thesis: c / b <= c / a
then a " >= b " by Lm37;
then (a " ) * c >= (b " ) * c by A1, Lm12;
then c / a >= (b " ) * c by XCMPLX_0:def 9;
hence c / b <= c / a by XCMPLX_0:def 9; :: thesis: verum