let z1, z2, z3 be quaternion number ; :: thesis: - ((z1 - z2) - z3) = ((- z1) + z2) + z3
A1: - ((z1 - z2) - z3) = (- (z1 - z2)) + z3 by Th57
.= ((- z1) + z2) + z3 by Th57 ;
thus - ((z1 - z2) - z3) = ((- z1) + z2) + z3 by A1; :: thesis: verum