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