reconsider xx = x as Surreal by A1;
let m1, m2 be Surreal; :: thesis: ( ( for x1 being Surreal st x1 = x holds
m1 = - x1 ) & ( for x1 being Surreal st x1 = x holds
m2 = - x1 ) implies m1 = m2 )
assume that
A2: for x1 being Surreal st x1 = x holds
m1 = - x1 and
A3: for x1 being Surreal st x1 = x holds
m2 = - x1 ; :: thesis: m1 = m2
m1 = - xx by A2;
hence m1 = m2 by A3; :: thesis: verum