theorem :: QUATERNI:78

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