theorem :: QUATERN3:44

for z1, z2 being Quaternion holds |.z1.| + |.z2.| >= (|.(z1 + z2).| + |.(z2 - z1).|) / 2