let x, y be Surreal; :: thesis: ( |.y.| infinitely< x implies not x + y == 0_No )
assume A1: |.y.| infinitely< x ; :: thesis: not x + y == 0_No
then A2: |.y.| < x by Th9;

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

suppose A3: 0_No <= y ; :: thesis: not x + y == 0_No

then y < x by A2, Def6;
then A4: y + y < x + y by SURREALR:44;
( 0_No = 0_No + 0_No & 0_No + 0_No <= y + y ) by A3, SURREALR:43;
hence not x + y == 0_No by A4, SURREALO:4; :: thesis: verum

end;

suppose y < 0_No ; :: thesis: not x + y == 0_No

then |.y.| = - y by Def6;
then A5: (- y) + y < x + y by A1, Th9, SURREALR:44;
y - y == 0_No by SURREALR:39;
hence not x + y == 0_No by A5, SURREALO:4; :: thesis: verum

end;

end;