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