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