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