let z1, z2 be quaternion number ; :: thesis: z1 - z2 = - (z2 - z1)
( Rea (z2 - z1) = (Rea z2) - (Rea z1) & Im1 (z2 - z1) = (Im1 z2) - (Im1 z1) & Im2 (z2 - z1) = (Im2 z2) - (Im2 z1) & Im3 (z2 - z1) = (Im3 z2) - (Im3 z1) ) by Lm34;
hence z1 - z2 = - (z2 - z1) ; :: thesis: verum