let x be R_eal; :: thesis: x + (- x) = 0.

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

suppose x in REAL ; :: thesis: x + (- x) = 0.

then consider a being Real such that
A1: ( x = a & - x = - a ) by SUPINF_2:def 3;
( x + (- x) = a + (- a) & (- x) + x = (- a) + a ) by A1, SUPINF_2:1;
hence x + (- x) = 0. ; :: thesis: verum

end;

suppose x = -infty ; :: thesis: x + (- x) = 0.

hence x + (- x) = 0. by SUPINF_1:6, SUPINF_2:4, SUPINF_2:def 2; :: thesis: verum

end;

suppose x = +infty ; :: thesis: x + (- x) = 0.

hence x + (- x) = 0. by SUPINF_1:6, SUPINF_2:4, SUPINF_2:def 2; :: thesis: verum

end;

end;