assume A1: x = a ; :: thesis: - x = - a
reconsider x1 = x as Element of QUATERNION by Def9;
reconsider b = - x1 as Element of G_Quaternion by Def9;
b + x = 0. G_Quaternion by Th35, QUATERNI:def 8;
hence - x = - a by A1, RLVECT_1:6; :: thesis: verum