let x, y be Surreal; :: thesis: |.(|.x.| - |.y.|).| <= |.(x - y).|
y - y == 0_No by SURREALR:39;
then ( x = x + 0_No & x + 0_No == x + (y + (- y)) & x + (y + (- y)) = (x + (- y)) + y ) by SURREALR:43, SURREALR:37;
then ( |.x.| == |.((x + (- y)) + y).| & |.((x + (- y)) + y).| <= |.(x + (- y)).| + |.y.| ) by Th37, Th48;
then |.x.| <= |.(x + (- y)).| + |.y.| by SURREALO:4;
then A1: |.x.| - |.y.| <= |.(x + (- y)).| by SURREALR:42;
x - x == 0_No by SURREALR:39;
then ( y = y + 0_No & y + 0_No == y + (x + (- x)) & y + (x + (- x)) = (y + (- x)) + x ) by SURREALR:43, SURREALR:37;
then ( |.y.| == |.((y + (- x)) + x).| & |.((y + (- x)) + x).| <= |.(y + (- x)).| + |.x.| ) by Th37, Th48;
then A2: |.y.| <= |.(y + (- x)).| + |.x.| by SURREALO:4;
- (x + (- y)) = (- x) + (- (- y)) by SURREALR:40
.= (- x) + y ;
then ( |.(y + (- x)).| = |.(- (x + (- y))).| & |.(- (x + (- y))).| == |.(x + (- y)).| ) by Th39, Th38;
then |.(y + (- x)).| + |.x.| == |.(x + (- y)).| + |.x.| by SURREALR:43;
then |.y.| <= |.(x + (- y)).| + |.x.| by A2, SURREALO:4;
then ( (- |.(x - y).|) - |.x.| = - (|.(x - y).| + |.x.|) & - (|.(x - y).| + |.x.|) <= - |.y.| ) by SURREALR:40, SURREALR:10;
then - |.(x - y).| <= |.x.| - |.y.| by SURREALR:42;
hence |.(|.x.| - |.y.|).| <= |.(x - y).| by A1, Th35; :: thesis: verum