let a, b be Real; :: thesis: ( b < 0 & a < b implies b " < a " )
A1: a " = 1 / a by XCMPLX_1:215;
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:87;
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