theorem :: SERIES_3:26

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