defpred S₁[ object , object ] means ( $1 is Surreal & ( for x being Surreal st x = $1 holds
$2 = - x ) );
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 xx = x as Surreal by A2;
( y = - xx & - xx = 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 & S₁[y,x] ) ) from TARSKI:sch 1(A1);
take M ; :: thesis: for o being object holds
( o in M iff ex x being Surreal st
( x in X & o = - x ) )
let y be object ; :: thesis: ( y in M iff ex x being Surreal st
( x in X & y = - x ) )
thus ( y in M implies ex x being Surreal st
( x in X & y = - x ) ) :: thesis: ( ex x being Surreal st
( x in X & y = - x ) implies y in M )

proof

assume y in M ; :: thesis: ex x being Surreal st
( x in X & y = - x )
then consider yy being object such that
A4: ( yy in X & S₁[yy,y] ) by A3;
reconsider yy = yy as Surreal by A4;
take yy ; :: thesis: ( yy in X & y = - yy )
thus ( yy in X & y = - yy ) by A4; :: thesis: verum

end;

given x being Surreal such that A5: ( x in X & y = - x ) ; :: thesis: y in M
S₁[x,y] by A5;
hence y in M by A5, A3; :: thesis: verum