let x, y be R_eal; :: thesis: |.(x + y).| <= |.x.| + |.y.|
A1: ( - |.x.| <= x & - |.y.| <= y ) by Th57;
A2: ( x <= |.x.| & y <= |.y.| ) by Th57;
A6: (- |.x.|) - |.y.| = - (|.x.| + |.y.|) by XXREAL_3:26;
( x + y <= |.x.| + |.y.| & (- |.x.|) + (- |.y.|) <= x + y ) by A1, A2, XXREAL_3:38;
hence |.(x + y).| <= |.x.| + |.y.| by A6, Th60; :: thesis: verum