theorem :: QUATERN3:36

for z1, z2, z3 being Quaternion holds |.((z1 + z2) - z3).| <= (|.z1.| + |.z2.|) + |.z3.|