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;

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

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;

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

then reconsider a = x as Real ;
A2: |.x.| = |.a.| ;

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

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;

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;

end;

end;

end;