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

reconsider x = x, y = y as R_eal by XXREAL_0:def 1;

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 ) )
;

end;

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;hence |.(x - y).| <= |.x.| + |.y.| by XXREAL_0:3; :: thesis: verum

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

then reconsider a = x as Element of REAL by XXREAL_0:14;

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

end;

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;hence |.(x - y).| <= |.x.| + |.y.| by A2, Th19, XXREAL_3:def 2; :: thesis: verum

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;hence |.(x - y).| <= |.x.| + |.y.| by A3, Th19, XXREAL_3:def 2; :: thesis: verum

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