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