reconsider b9 = - b as Element of INT.Ring by INT_1:def 2;
assume b = a ; :: thesis: - a = - b
then b9 + a = 0. INT.Ring ;
hence - a = - b by RLVECT_1:6; :: thesis: verum