let c1, c2 be Quaternion; :: thesis: c1 = (c1 + c2) - c2
thus (c1 + c2) - c2 = c1 + (c2 - c2) by Th2
.= c1 + 0q by QUATERNI:def 8
.= c1 by Th3 ; :: thesis: verum