let x be Surreal; :: thesis: ( x == 0_No iff |.x.| == 0_No )
thus ( x == 0_No implies |.x.| == 0_No ) by Def6; :: thesis: ( |.x.| == 0_No implies x == 0_No )
assume A1: |.x.| == 0_No ; :: thesis: x == 0_No
thus x <= 0_No by A1, Def6; :: according to SURREALO:def 2 :: thesis: 0_No <= x
assume x < 0_No ; :: thesis: contradiction
then ( 0_No = - 0_No & - 0_No < - x & |.x.| = - x ) by Def6, SURREALR:10;
hence contradiction by A1; :: thesis: verum