let x be Surreal; :: thesis: ( - |.x.| <= x & x <= |.x.| )

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

suppose A1: 0_No <= x ; :: thesis: ( - |.x.| <= x & x <= |.x.| )

then A2: |.x.| = x by Def6;
( - x <= - 0_No & - 0_No = 0_No ) by A1, SURREALR:10;
hence ( - |.x.| <= x & x <= |.x.| ) by A2, A1, SURREALO:4; :: thesis: verum

end;

suppose A3: x < 0_No ; :: thesis: ( - |.x.| <= x & x <= |.x.| )

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

end;

end;