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