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