let I1, I2 be Surreal; :: thesis: ( ( x is positive & I1 = inv x & I2 = inv x implies I1 = I2 ) & ( not x is positive & - I1 = inv (- x) & - I2 = inv (- x) implies I1 = I2 ) )
( I1 = - (- I1) & I2 = - (- I2) ) ;
hence ( ( x is positive & I1 = inv x & I2 = inv x implies I1 = I2 ) & ( not x is positive & - I1 = inv (- x) & - I2 = inv (- x) implies I1 = I2 ) ) ; :: thesis: verum