let x be ExtReal; :: thesis: ( x = - x implies x = 0 )

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

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

hence ( x = - x implies x = 0 ) ; :: thesis: verum

end;

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

then reconsider y = x as Element of REAL ;
- x = - y by XXREAL_3:def 3;
hence ( x = - x implies x = 0 ) ; :: thesis: verum

end;

end;