let x, y be ExtReal; :: thesis: ( ( x is Real or y is Real ) implies |.x.| - |.y.| <= |.(x - y).| )

assume A1: ( x is Real or y is Real ) ; :: thesis: |.x.| - |.y.| <= |.(x - y).|

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

assume A1: ( x is Real or y is Real ) ; :: thesis: |.x.| - |.y.| <= |.(x - y).|

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

per cases
( y is Real or x is Real )
by A1;

end;

suppose
y is Real
; :: thesis: |.x.| - |.y.| <= |.(x - y).|

then
(x - y) + y = x
by XXREAL_3:22;

then |.x.| <= |.(x - y).| + |.y.| by Th13;

hence |.x.| - |.y.| <= |.(x - y).| by XXREAL_3:42; :: thesis: verum

end;then |.x.| <= |.(x - y).| + |.y.| by Th13;

hence |.x.| - |.y.| <= |.(x - y).| by XXREAL_3:42; :: thesis: verum

suppose
x is Real
; :: thesis: |.x.| - |.y.| <= |.(x - y).|

then reconsider a = x as Real ;

A2: |.x.| = |.a.| ;

end;A2: |.x.| = |.a.| ;

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

end;

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

|.y.| = +infty
by Th19, A3;

then |.x.| - |.y.| = -infty by A2, XXREAL_3:13;

then |.x.| - |.y.| <= |.(x - y).| ;

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

end;then |.x.| - |.y.| = -infty by A2, XXREAL_3:13;

then |.x.| - |.y.| <= |.(x - y).| ;

hence |.x.| - |.y.| <= |.(x - y).| ; :: 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 - y = a - b by SUPINF_2:3;

then A4: |.(x - y).| = |.(a - b).| by Th1;

|.y.| = |.b.| by Th1;

then |.x.| - |.y.| = |.a.| - |.b.| by A2, SUPINF_2:3;

hence |.x.| - |.y.| <= |.(x - y).| by A4, COMPLEX1:59; :: thesis: verum

end;x - y = a - b by SUPINF_2:3;

then A4: |.(x - y).| = |.(a - b).| by Th1;

|.y.| = |.b.| by Th1;

then |.x.| - |.y.| = |.a.| - |.b.| by A2, SUPINF_2:3;

hence |.x.| - |.y.| <= |.(x - y).| by A4, COMPLEX1:59; :: thesis: verum