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 )

0_No <= |.x.| by Th31;
then 0_No < y by A2, SURREALO:4;
then ( - y < - 0_No & - 0_No = 0_No ) by SURREALR:10;
hence ( - y < x & x < y ) by A2, A4, Def6, 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;