let x, y be R_eal; :: thesis: ( ( x = +infty & y = -infty ) or ( x = -infty & y = +infty ) or |.(x + y).| <= |.x.| + |.y.| )
assume A1: ( not ( x = +infty & y = -infty ) & not ( x = -infty & y = +infty ) ) ; :: thesis: |.(x + y).| <= |.x.| + |.y.|
A2: ( - |.x.| <= x & x <= |.x.| & - |.y.| <= y & 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 ( +infty <= |.x.| & y <> -infty & -infty <= y ) by A1, Th57, XXREAL_0:5;
then A4: ( |.x.| = +infty & -infty < y ) by XXREAL_0:1, XXREAL_0:4;

now

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

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

(- |.x.|) - |.y.| = - (|.x.| + |.y.|) by XXREAL_3:26;
hence |.(x + y).| <= |.x.| + |.y.| by A3, A4, A5, Th60; :: thesis: verum

end;

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

A8: x + y <= |.x.| + |.y.| by A2, XXREAL_3:38;
A10: (- |.x.|) + (- |.y.|) <= x + y by A2, XXREAL_3:38;
(- |.x.|) - |.y.| = - (|.x.| + |.y.|) by XXREAL_3:26;
hence |.(x + y).| <= |.x.| + |.y.| by A8, A10, Th60; :: thesis: verum

end;

end;

end;

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

end;

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

now

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

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

then A14: - |.y.| = -infty by Th57, XXREAL_0:6;
A15: x + y <= |.x.| + |.y.| by A2, XXREAL_3:38;
(- |.x.|) - |.y.| = - (|.x.| + |.y.|) by XXREAL_3:26;
hence |.(x + y).| <= |.x.| + |.y.| by A11, A13, A14, A15, Th60; :: thesis: verum

end;

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

A17: x + y <= |.x.| + |.y.| by A2, XXREAL_3:38;
A18: (- |.x.|) + (- |.y.|) <= x + y by A2, XXREAL_3:38;
(- |.x.|) - |.y.| = - (|.x.| + |.y.|) by XXREAL_3:26;
hence |.(x + y).| <= |.x.| + |.y.| by A17, A18, Th60; :: thesis: verum

end;

end;

end;

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

end;

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

A21: x + y <= |.x.| + |.y.| by A2, XXREAL_3:38;
A22: (- |.x.|) + (- |.y.|) <= x + y by A2, XXREAL_3:38;
(- |.x.|) - |.y.| = - (|.x.| + |.y.|) by XXREAL_3:26;
hence |.(x + y).| <= |.x.| + |.y.| by A21, A22, Th60; :: thesis: verum

end;

end;