assume A1: x = a ; :: thesis: - a = - x
reconsider b = - x as Element of F_Real by XREAL_0:def 1;
b + a = 0. F_Real by A1;
hence - a = - x by RLVECT_1:19; :: thesis: verum