+ (0,0) = 0 by ARYTM_0:11;
hence opp 0 = 0 by ARYTM_0:def 3; :: thesis: verum