+ (0,0) = 0 by ARYTM_0:13;
hence opp 0 = 0 by ARYTM_0:def 4; :: thesis: verum