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