let a, b, c be Real; :: thesis: ( 0 < c & b < 0 & a < b implies c / b < c / a )
assume that
A1: c > 0 and
A2: b < 0 and
A3: a < b ; :: thesis: c / b < c / a
a " > b " by A2, A3, Lm31;
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