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