let x be ExtReal; :: 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 Th5; :: thesis: verum

end;

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

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

end;

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

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

end;

end;