let x, y, z, w be Real; :: thesis: ( |.(x - y).| < |.(z - w).| & x + y = z + w implies x * y > z * w )
assume A1: ( |.(x - y).| < |.(z - w).| & x + y = z + w ) ; :: thesis: x * y > z * w
(x - y) ^2 < (z - w) ^2 by A1, ProdMon;
then ((x + y) ^2) - ((x - y) ^2) > ((z + w) ^2) - ((z - w) ^2) by A1, XREAL_1:15;
then 4 * (x * y) > 4 * (z * w) ;
hence x * y > z * w by XREAL_1:64; :: thesis: verum