let b, a be real number ; :: thesis: ( b < 0 & a < b implies b " < a " )
A1: a " = 1 / a by XCMPLX_1:217;
assume that
A2: 0 > b and
A3: a < b ; :: thesis: b " < a "
b * (a " ) < a * (a " ) by A2, A3, Lm24;
then b * (a " ) < 1 by A1, A2, A3, XCMPLX_1:88;
then (b " ) * (b * (a " )) > 1 * (b " ) by A2, Lm24;
then ((b " ) * b) * (a " ) > 1 * (b " ) ;
then 1 * (a " ) > 1 * (b " ) by A2, XCMPLX_0:def 7;
hence b " < a " ; :: thesis: verum