for x, y, z, w being ExtReal st x < y & w < z holds
x + w < y + z