defpred S₁[ object , object ] means ( L_ $1 is Surreal & $1 `2 is Surreal & ( for x, y being Surreal st x = L_ $1 & y = $1 `2 holds
$2 = x + y ) );
A1: for x, y, z being object st S₁[x,y] & S₁[x,z] holds
y = z

proof

let x, y, z be object ; :: thesis: ( S₁[x,y] & S₁[x,z] implies y = z )
assume A2: ( S₁[x,y] & S₁[x,z] ) ; :: thesis: y = z
reconsider x1 = L_ x, x2 = R_ x as Surreal by A2;
( y = x1 + x2 & x1 + x2 = z ) by A2;
hence y = z ; :: thesis: verum

end;

consider M being set such that
A3: for x being object holds
( x in M iff ex y being object st
( y in [:X,Y:] & S₁[y,x] ) ) from TARSKI:sch 1(A1);
take M ; :: thesis: for o being object holds
( o in M iff ex x, y being Surreal st
( x in X & y in Y & o = x + y ) )
let a be object ; :: thesis: ( a in M iff ex x, y being Surreal st
( x in X & y in Y & a = x + y ) )
thus ( a in M implies ex x, y being Surreal st
( x in X & y in Y & a = x + y ) ) :: thesis: ( ex x, y being Surreal st
( x in X & y in Y & a = x + y ) implies a in M )

proof

assume a in M ; :: thesis: ex x, y being Surreal st
( x in X & y in Y & a = x + y )
then consider yy being object such that
A4: ( yy in [:X,Y:] & S₁[yy,a] ) by A3;
reconsider y1 = L_ yy, y2 = R_ yy as Surreal by A4;
take y1 ; :: thesis: ex y being Surreal st
( y1 in X & y in Y & a = y1 + y )
take y2 ; :: thesis: ( y1 in X & y2 in Y & a = y1 + y2 )
yy is pair by A4;
hence ( y1 in X & y2 in Y & a = y1 + y2 ) by A4, ZFMISC_1:87; :: thesis: verum

end;

given x, y being Surreal such that A5: ( x in X & y in Y & a = x + y ) ; :: thesis: a in M
A6: [x,y] in [:X,Y:] by A5, ZFMISC_1:87;
S₁[[x,y],a] by A5;
hence a in M by A6, A3; :: thesis: verum