theorem :: RVSUM_3:2

for x, y, z, w being Real st |.(x - y).| < |.(z - w).| & x + y = z + w holds
x * y > z * w