let z1, z2, z3 be Quaternion; :: thesis: - ((z1 + z2) + z3) = ((- z1) - z2) - z3
- ((z1 + z2) + z3) = - (z1 + (z2 + z3)) by QUATERN2:2
.= (- z1) - (z2 + z3) by Th52
.= ((- z1) - z2) - z3 by Th54 ;
hence - ((z1 + z2) + z3) = ((- z1) - z2) - z3 ; :: thesis: verum