let x be Element of REAL ; :: thesis: opp x = - x
+ (x,(opp x)) = 0 by ARYTM_0:def 3;
then x + (opp x) = 0 by Lm8;
hence opp x = - x ; :: thesis: verum