let a, b be Real; :: thesis: ( a * b is positive implies |.(a - b).| < |.(a + b).| )
assume A1: a * b is positive ; :: 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 b > 0 by A1;
then ( (a - b) + (2 * b) > (a - b) + 0 & (b - a) + (2 * a) > (b - a) + 0 ) by B1, XREAL_1:6;
hence |.(a - b).| < |.(a + b).| by 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;