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