reconsider b = - x as Element of F_Real ;
assume x = a ; :: thesis: - a = - x
then b + a = 0. F_Real ;
hence - a = - x by RLVECT_1:6; :: thesis: verum