let a, b be Real; :: thesis: ( a * b is negative implies |.(a - b).| > |.(a + b).| )
assume A1: a * b is negative ; :: thesis: |.(a - b).| > |.(a + b).|
A2: ( |.(a - b).| = a - b or |.(a - b).| = - (a - b) ) by ABSVALUE:def 1;

per cases ( a = 0 or a > 0 or a < 0 ) ;

suppose a = 0 ; :: thesis: |.(a - b).| > |.(a + b).|

hence |.(a - b).| > |.(a + b).| by A1; :: thesis: verum

end;

suppose B1: a > 0 ; :: thesis: |.(a - b).| > |.(a + b).|

then B2: b < 0 by A1;
then ( (a - b) + (2 * b) < (a - b) + 0 & (- (a - b)) + (2 * a) > (- (a - b)) + 0 ) by B1, XREAL_1:6;
then ( a + b < a - b & - (a + b) < - (- (a - b)) ) by XREAL_1:24;
hence |.(a - b).| > |.(a + b).| by B1, B2, A2, ABSVALUE:def 1; :: thesis: verum

end;

suppose B1: a < 0 ; :: thesis: |.(a - b).| > |.(a + b).|

then B2: b > 0 by A1;
then ( (a - b) + (2 * b) > (a - b) + 0 & (b - a) + (2 * a) < (b - a) + 0 ) by B1, XREAL_1:6;
then ( - (a + b) < - (a - b) & a + b < b - a ) by XREAL_1:24;
hence |.(a - b).| > |.(a + b).| by B1, B2, A2, ABSVALUE:def 1; :: thesis: verum

end;

end;