theorem Th76: :: QUATERNI:83
for z1, z2 being Quaternion holds |.(z1 - z2).| = |.(z2 - z1).|