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.|
A3: |.b.| = - b by A1, A2, ABSVALUE:def 1;

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

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

hence |.a.| < |.b.| by A1; :: thesis: verum

end;

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

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

end;

end;