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

A1: |.y.| - |.x.| = - (|.x.| - |.y.|) by XXREAL_3:26;

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

then A3: |.x.| - |.y.| <= |.(x - y).| by Th20;

y - x = - (x - y) by XXREAL_3:26;

then A4: |.(y - x).| = |.(x - y).| by Th18;

|.y.| - |.x.| <= |.(y - x).| by A2, Th20;

then - |.(x - y).| <= - (- (|.x.| - |.y.|)) by A4, A1, XXREAL_3:38;

hence |.(|.x.| - |.y.|).| <= |.(x - y).| by A3, Th12; :: thesis: verum

A1: |.y.| - |.x.| = - (|.x.| - |.y.|) by XXREAL_3:26;

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

then A3: |.x.| - |.y.| <= |.(x - y).| by Th20;

y - x = - (x - y) by XXREAL_3:26;

then A4: |.(y - x).| = |.(x - y).| by Th18;

|.y.| - |.x.| <= |.(y - x).| by A2, Th20;

then - |.(x - y).| <= - (- (|.x.| - |.y.|)) by A4, A1, XXREAL_3:38;

hence |.(|.x.| - |.y.|).| <= |.(x - y).| by A3, Th12; :: thesis: verum