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