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

per cases ( |.x.| = x or |.x.| = - x ) by Def6;

suppose |.x.| = x ; :: thesis: not x + y == 0_No

hence not x + y == 0_No by A1, Th44; :: thesis: verum

end;

suppose |.x.| = - x ; :: thesis: not x + y == 0_No

then A2: |.(- y).| infinitely< - x by Th40, Th17, A1;
(- x) + (- y) = - (x + y) by SURREALR:40;
hence not x + y == 0_No by A2, Th44, SURREALR:24; :: thesis: verum

end;

end;