assume A1: a = r ; :: thesis: - a = - r
reconsider b = - r as Element of N_Real by XREAL_0:def 1;
b + a = 0. N_Real by A1;
hence - a = - r by ALGSTR_0:def 13; :: thesis: verum