reconsider c = |.(Im a).| as non negative Real ;
( - |.a.| <= Im a & Im a <= |.a.| ) by COMPLEX1:55, COMPLEX155a;
then c <= |.a.| by ABSVALUE:5;
hence not |.(Im a).| is heavy by Def3; :: thesis: verum