theorem :: QUATERNI:76

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