theorem :: EXTREAL1:34

for x, y, w, z being ExtReal st |.x.| <= z & |.y.| <= w holds
|.(x + y).| <= z + w