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;

per cases ( x = +infty or x = -infty or ( x <> +infty & x <> -infty ) ) ;

suppose A3: x = +infty ; :: thesis: |.(x + y).| <= |.x.| + |.y.|

then A4: |.x.| = +infty by Th57, XXREAL_0:4;

now

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

end;

hence |.(x + y).| <= |.x.| + |.y.| ; :: thesis: verum

end;

suppose A7: x = -infty ; :: thesis: |.(x + y).| <= |.x.| + |.y.|

now

per cases ( y = -infty or y <> -infty ) ;

suppose A8: y = -infty ; :: thesis: |.(x + y).| <= |.x.| + |.y.|

A9: ( x + y <= |.x.| + |.y.| & (- |.x.|) - |.y.| = - (|.x.| + |.y.|) ) by A2, XXREAL_3:26, XXREAL_3:38;
- |.y.| = -infty by A8, Th57, XXREAL_0:6;
hence |.(x + y).| <= |.x.| + |.y.| by A7, A8, A9, Th60; :: thesis: verum

end;

suppose y <> -infty ; :: thesis: |.(x + y).| <= |.x.| + |.y.|

A10: (- |.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 A10, Th60; :: thesis: verum

end;

end;

end;

hence |.(x + y).| <= |.x.| + |.y.| ; :: thesis: verum

end;

suppose ( x <> +infty & x <> -infty ) ; :: thesis: |.(x + y).| <= |.x.| + |.y.|

A11: (- |.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 A11, Th60; :: thesis: verum

end;

end;