let x, y be ExtReal; :: thesis: ( x + y = 0 implies x = - y )
assume A1: x + y = 0 ; :: thesis: x = - y

per cases ( x in REAL or x = -infty or x = +infty ) by XXREAL_0:14;

suppose x in REAL ; :: thesis: x = - y

then reconsider x = x as Real ;
x + y is real by A1;
then reconsider y = y as Real ;
x + y = 0 by A1;
then x = - y ;
hence x = - y ; :: thesis: verum

end;

suppose A2: x = -infty ; :: thesis: x = - y

then y = +infty by A1, Def2;
hence x = - y by A2, Def3; :: thesis: verum

end;

suppose A3: x = +infty ; :: thesis: x = - y

then y = -infty by A1, Def2;
hence x = - y by A3, Def3; :: thesis: verum

end;

end;