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;