let M1, M2 be set ; :: thesis: ( ( for o being object holds
( o in M1 iff ex x being Surreal st
( x in X & o = - x ) ) ) & ( for o being object holds
( o in M2 iff ex x being Surreal st
( x in X & o = - x ) ) ) implies M1 = M2 )
assume that
A6: for y being object holds
( y in M1 iff ex x being Surreal st
( x in X & y = - x ) ) and
A7: for y being object holds
( y in M2 iff ex x being Surreal st
( x in X & y = - x ) ) ; :: thesis: M1 = M2

now :: thesis: for y being object holds
( y in M1 iff y in M2 )

let y be object ; :: thesis: ( y in M1 iff y in M2 )
( y in M1 iff ex x being Surreal st
( x in X & y = - x ) ) by A6;
hence ( y in M1 iff y in M2 ) by A7; :: thesis: verum

end;

hence M1 = M2 by TARSKI:2; :: thesis: verum