theorem :: QUATERNI:77

for z being Quaternion holds Im2 z <= |.z.|