let x, y be ExtReal; :: thesis: |.(x - y).| <= |.x.| + |.y.|
reconsider x = x, y = y as R_eal by XXREAL_0:def 1;

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 Th19, XXREAL_3:def 2;
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 Element of 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 Element of REAL by XXREAL_0:14;
( |.x.| = |.a.| & |.y.| = |.b.| ) by Th1;
then A4: |.x.| + |.y.| = |.a.| + |.b.| by SUPINF_2:1;
x - y = a - b by SUPINF_2:3;
then |.(x - y).| = |.(a - b).| by Th1;
hence |.(x - y).| <= |.x.| + |.y.| by A4, COMPLEX1:57; :: thesis: verum

end;

end;

end;

end;