let x, y be Surreal; :: thesis: ( ( - y <= x & x <= y ) iff |.x.| <= y )
thus ( - y <= x & x <= y implies |.x.| <= y ) :: thesis: ( |.x.| <= y implies ( - y <= x & x <= y ) )

proof

assume A1: ( - y <= x & x <= y ) ; :: thesis: |.x.| <= y
then ( - x <= - (- y) & - (- y) = y ) by SURREALR:10;
hence |.x.| <= y by A1, Def6; :: thesis: verum

end;

assume A2: |.x.| <= y ; :: thesis: ( - y <= x & x <= y )
0_No <= |.x.| by Th31;
then A3: 0_No <= y by A2, SURREALO:4;

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

suppose A4: 0_No <= x ; :: thesis: ( - y <= x & x <= y )

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

end;

suppose A5: x < 0_No ; :: thesis: ( - y <= x & x <= y )

then - x <= - (- y) by A2, Def6;
hence ( - y <= x & x <= y ) by SURREALR:10, A3, A5, SURREALO:4; :: thesis: verum

end;

end;