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