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

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

let z be object ; :: thesis: ( z in M1 iff z in M2 )
( z in M1 iff ex x, y being Surreal st
( x in X & y in Y & z = x + y ) ) by A7;
hence ( z in M1 iff z in M2 ) by A8; :: thesis: verum

end;

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