theorem ProdMon: :: RVSUM_3:1

for x, y, z, w being Real st |.(x - y).| < |.(z - w).| holds
(x - y) ^2 < (z - w) ^2