let a, b be Real; :: thesis: ( b <= a & a <= 0 implies |.a.| <= |.b.| )
assume that
A1: b <= a and
A2: a <= 0 ; :: thesis: |.a.| <= |.b.|

per cases ( a = 0 or a < 0 ) by A2;

suppose a = 0 ; :: thesis: |.a.| <= |.b.|

then |.a.| = 0 by ABSVALUE:2;
hence |.a.| <= |.b.| by COMPLEX1:46; :: thesis: verum

end;

suppose A3: a < 0 ; :: thesis: |.a.| <= |.b.|

then A4: |.a.| = - a by ABSVALUE:def 1;
|.b.| = - b by A1, A3, ABSVALUE:def 1;
hence |.a.| <= |.b.| by A1, A4, XREAL_1:24; :: thesis: verum

end;

end;