theorem Th13: :: EXTREAL1:24

for x, y being ExtReal holds |.(x + y).| <= |.x.| + |.y.|