let x be Surreal; :: thesis: ( not x == 0_No implies |.(- x).| = |.x.| )
assume not x == 0_No ; :: thesis: |.(- x).| = |.x.|

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

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

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

end;

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

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

end;

end;