let x, y be ext-real number ; :: thesis: ( x + y = 0 implies x = - y )
assume Z: 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 number ;
x + y is real by Z;
then reconsider y = y as real number ;
x + y = 0 by Z;
then x = - y ;
hence x = - y ; :: thesis: verum

end;

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

then y = +infty by Z, Def3;
hence x = - y by S, Def5; :: thesis: verum

end;

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

then y = -infty by Z, Def3;
hence x = - y by S, Def5; :: thesis: verum

end;

end;