let x, y be R_eal; :: thesis: |.(x - y).| <= |.x.| + |.y.|

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

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

then |.x.| + |.y.| = +infty by XXREAL_3:def 2, Th19;
hence |.(x - y).| <= |.x.| + |.y.| by XXREAL_0:3; :: thesis: verum

end;

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

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

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

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

x - y = -infty by A1, A2, XXREAL_3:13;
hence |.(x - y).| <= |.x.| + |.y.| by A2, Th19, XXREAL_3:def 2; :: thesis: verum

end;

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

x - y = +infty by A1, A3, XXREAL_3:14;
hence |.(x - y).| <= |.x.| + |.y.| by A3, Th19, 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.| = abs a & |.y.| = abs b ) by Th1;
then A4: |.x.| + |.y.| = (abs a) + (abs b) by SUPINF_2:1;
x - y = a - b by SUPINF_2:3;
then |.(x - y).| = abs (a - b) by Th1;
hence |.(x - y).| <= |.x.| + |.y.| by A4, COMPLEX1:57; :: thesis: verum

end;

end;

end;

end;