let x, y, z be Surreal; :: thesis: ( x <= y & y <= z implies |.y.| <= |.x.| + |.z.| )
assume A1: ( x <= y & y <= z ) ; :: thesis: |.y.| <= |.x.| + |.z.|

per cases ( 0_No <= y or y < 0_No ) ;

suppose 0_No <= y ; :: thesis: |.y.| <= |.x.| + |.z.|

then A2: ( |.y.| = y & |.z.| = z ) by A1, SURREALO:4, Def6;
0_No <= |.x.| by Th31;
then ( |.z.| = 0_No + |.z.| & 0_No + |.z.| <= |.x.| + |.z.| ) by SURREALR:43;
hence |.y.| <= |.x.| + |.z.| by A2, A1, SURREALO:4; :: thesis: verum

end;

suppose A3: y < 0_No ; :: thesis: |.y.| <= |.x.| + |.z.|

then x < 0_No by A1, SURREALO:4;
then ( |.y.| = - y & |.x.| = - x ) by A3, Def6;
then A4: |.y.| <= |.x.| by A1, SURREALR:10;
0_No <= |.z.| by Th31;
then ( |.x.| = 0_No + |.x.| & 0_No + |.x.| <= |.x.| + |.z.| ) by SURREALR:43;
hence |.y.| <= |.x.| + |.z.| by A4, SURREALO:4; :: thesis: verum

end;

end;