let z1, z2, z3 be quaternion number ; :: thesis: - ((z1 + z2) - z3) = ((- z1) - z2) + z3
- ((z1 + z2) - z3) = (- (z1 + z2)) + z3 by t2
.= ((- z1) - z2) + z3 by t1 ;
hence - ((z1 + z2) - z3) = ((- z1) - z2) + z3 ; :: thesis: verum