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

assume b = a ; :: thesis: - a = - b

then b9 + a = 0. INT.Ring ;

hence - a = - b by RLVECT_1:6; :: thesis: verum