let z1, z2 be Quaternion; :: thesis: |.(z1 - z2).| = |.(z2 - z1).|
thus |.(z1 - z2).| = |.(- (z2 - z1)).| by Lm37
.= |.(z2 - z1).| by Th65 ; :: thesis: verum