let a, b be Real; :: thesis: ( b < 0 & a <= b implies b " <= a " )
assume that
A1: 0 > b and
A2: a <= b ; :: thesis: b " <= a "
b * (a ") <= a * (a ") by A1, A2, Lm28;
then b * (a ") <= 1 by A1, A2, XCMPLX_0:def 7;
then (b ") * (b * (a ")) >= 1 * (b ") by A1, Lm28;
then ((b ") * b) * (a ") >= 1 * (b ") ;
then 1 * (a ") >= 1 * (b ") by A1, XCMPLX_0:def 7;
hence b " <= a " ; :: thesis: verum