let x, y be Surreal; :: thesis: ( x == y implies |.x.| == |.y.| )
assume A1: x == y ; :: thesis: |.x.| == |.y.|

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

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

then ( |.x.| = x & 0_No <= y ) by Def6, A1, SURREALO:4;
hence |.x.| == |.y.| by A1, Def6; :: thesis: verum

end;

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

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

end;

end;