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 Lm35;
then (a " ) * c > (b " ) * c by A1, Lm13;
then c / a > (b " ) * c by XCMPLX_0:def 9;
hence c / b < c / a by XCMPLX_0:def 9; :: thesis: verum