let x be ext-real number ; :: thesis: x + (- x) = 0

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

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

hence x + (- x) = 0 by Tx4A; :: thesis: verum

end;

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

then reconsider x = x as real number ;
reconsider y = - x as real number ;
x + y = 0 ;
hence x + (- x) = 0 ; :: thesis: verum

end;

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

hence x + (- x) = 0 by Tx4B; :: thesis: verum

end;

end;