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