let x, y, w, z be ExtReal; :: thesis: ( |.x.| <= z & |.y.| <= w implies |.(x + y).| <= z + w )
assume A1: ( |.x.| <= z & |.y.| <= w ) ; :: thesis: |.(x + y).| <= z + w
then ( - z <= x & - w <= y ) by Th12;
then A2: (- z) + (- w) <= x + y by XXREAL_3:36;
( x <= z & y <= w ) by A1, Th12;
then A3: x + y <= z + w by XXREAL_3:36;
(- z) - w = - (z + w) by XXREAL_3:25;
hence |.(x + y).| <= z + w by A3, A2, Th12; :: thesis: verum