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