theorem :: XXREAL_3:64

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