let x, y be Surreal; :: thesis: ( x - y == 0_No implies x == y )
A1: ( (- y) + y = y - y & y - y == 0_No ) by Th39;
assume x - y == 0_No ; :: thesis: x == y
then ( y = 0_No + y & 0_No + y == (x + (- y)) + y & (x + (- y)) + y = x + ((- y) + y) ) by Th37, Th43;
then ( y == x + ((- y) + y) & x + ((- y) + y) == x + 0_No & x + 0_No = x ) by A1, Th43;
hence x == y by SURREALO:4; :: thesis: verum