let x be ExtReal; :: thesis: ( x + x = 0 implies x = 0 )
assume x + x = 0 ; :: thesis: x = 0
then x = - x by XXREAL_3:8;
hence x = 0 by Th1; :: thesis: verum