theorem :: EXTREAL1:32

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