let x, y be R_eal; :: 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).|

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

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

then (x - y) + y = x by XXREAL_3:22;
then A3: |.x.| <= |.(x - y).| + |.y.| by Th61;
reconsider b = y as Real by A2;
|.y.| = abs b by Th49;
hence |.x.| - |.y.| <= |.(x - y).| by A3, XXREAL_3:42; :: thesis: verum

end;

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

then reconsider a = x as Real ;
A4: |.x.| = abs a by Th49;

now

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

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

then |.x.| - |.y.| < 0 by A4, Th67, XXREAL_3:13;
hence |.x.| - |.y.| <= |.(x - y).| by Th51; :: thesis: verum

end;

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

then reconsider b = y as Real by XXREAL_0:14;
x - y = a - b by SUPINF_2:3;
then A5: |.(x - y).| = abs (a - b) by Th49;
|.y.| = abs b by Th49;
then |.x.| - |.y.| = (abs a) - (abs b) by A4, SUPINF_2:3;
hence |.x.| - |.y.| <= |.(x - y).| by A5, COMPLEX1:59; :: thesis: verum

end;

end;

end;

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

end;

end;