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.|

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

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

then x - y = +infty by A1, XXREAL_3:13;
then A3: ( |.(x - y).| = +infty & |.x.| = +infty ) by A2, EXTREAL1:36;
( -infty < 0 & 0 <= |.y.| ) by Th51;
hence |.(x - y).| <= |.x.| + |.y.| by A3, XXREAL_3:def 2; :: thesis: verum

end;

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

then A5: x - y = -infty by A1, XXREAL_3:14;
( -infty < 0 & 0 <= |.y.| ) by Th51;
hence |.(x - y).| <= |.x.| + |.y.| by A4, A5, Th67, XXREAL_3:def 2; :: thesis: verum

end;

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

then reconsider a = x as Real by XXREAL_0:14;

now

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

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

then A8: x - y = -infty by A6, XXREAL_3:13;
( -infty < 0 & 0 <= |.x.| ) by Th51;
hence |.(x - y).| <= |.x.| + |.y.| by A7, A8, Th67, XXREAL_3:def 2; :: thesis: verum

end;

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

then A10: x - y = +infty by A6, XXREAL_3:14;
( -infty < 0 & 0 <= |.x.| ) by Th51;
hence |.(x - y).| <= |.x.| + |.y.| by A9, A10, Th67, XXREAL_3:def 2; :: thesis: verum

end;

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

then reconsider b = y as Real by XXREAL_0:14;
x - y = a - b by SUPINF_2:5;
then A11: ( |.(x - y).| = abs (a - b) & |.x.| = abs a & |.y.| = abs b ) by Th49;
then |.x.| + |.y.| = (abs a) + (abs b) by SUPINF_2:1;
hence |.(x - y).| <= |.x.| + |.y.| by A11, COMPLEX1:143; :: thesis: verum

end;

end;

end;

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

end;

end;