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

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

suppose A1: 0_No < x ; :: thesis: |.x.| is positive

then 0_No <= x ;
hence |.x.| is positive by A1, Def6; :: thesis: verum

end;

suppose A2: x < 0_No ; :: thesis: |.x.| is positive

then |.x.| = - x by Def6;
hence |.x.| is positive by A2, SURREALR:10, SURREALR:23; :: thesis: verum

end;

end;