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