let a, b, c be Real; :: thesis: ( c < 0 & a < b implies b / c < a / c )
assume that
A1: c < 0 and
A2: a < b ; :: thesis: b / c < a / c
a / (- c) < b / (- c) by A1, A2, Lm26;
then - (a / c) < b / (- c) by XCMPLX_1:188;
then - (a / c) < - (b / c) by XCMPLX_1:188;
hence b / c < a / c by Lm14; :: thesis: verum