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