reconsider b = - x as Element of G_Real by XREAL_0:def 1;

assume x = a ; :: thesis: - a = - x

then b + a = 0. G_Real ;

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

assume x = a ; :: thesis: - a = - x

then b + a = 0. G_Real ;

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