let x be Surreal; :: thesis: ( x == 0_No implies |.(- x).| == |.x.| )
assume A1: x == 0_No ; :: thesis: |.(- x).| == |.x.|
then ( - x == - 0_No & - 0_No = 0_No ) by SURREALR:10;
then ( |.(- x).| == 0_No & |.x.| == 0_No ) by A1, Def6;
hence |.(- x).| == |.x.| by SURREALO:4; :: thesis: verum