reconsider c = |.(Re a).| + |.(Im a).| as non negative Real ;
( c >= |.a.| & |.a.| > 1 ) by RI, Def1;
hence |.(Re a).| + |.(Im a).| is heavy by XXREAL_0:2; :: thesis: verum