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

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