let x, y be Surreal; :: thesis: ( not 0_No == x & x == y implies x " == y " )
assume A1: ( not 0_No == x & x == y ) ; :: thesis: x " == y "
then A2: not 0_No == y by SURREALO:4;
( y * (x ") == x * (x ") & x * (x ") == 1_No ) by A1, Th33, SURREALR:54;
then y * (x ") == 1_No by SURREALO:4;
hence x " == y " by A2, Th41; :: thesis: verum