let x be Surreal; :: thesis: 0_No <= |.x.|

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

suppose 0_No <= x ; :: thesis: 0_No <= |.x.|

hence 0_No <= |.x.| by Def6; :: thesis: verum

end;

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

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

end;

end;