let x, z, y, w be R_eal; :: thesis: ( |.x.| <= z & |.y.| <= w implies |.(x + y).| <= z + w )
assume that
A2: |.x.| <= z and
A3: |.y.| <= w ; :: thesis: |.(x + y).| <= z + w
A6: ( - z <= x & x <= z & - w <= y & y <= w ) by A2, A3, Th60;
then A7: x + y <= z + w by XXREAL_3:38;
A8: (- z) + (- w) <= x + y by A6, XXREAL_3:38;
(- z) - w = - (z + w) by XXREAL_3:26;
hence |.(x + y).| <= z + w by A7, A8, Th60; :: thesis: verum