per cases ( not Im a is negative or Im a is negative ) ;

suppose not Im a is negative ; :: thesis: Im a is light

then reconsider b = Im a as non negative Real ;
( Im a <= |.a.| & |.a.| < 1 ) by COMPLEX1:55, Def2;
then b < 1 by XXREAL_0:2;
hence Im a is light ; :: thesis: verum

end;

suppose Im a is negative ; :: thesis: Im a is light

then ( |.(Im a).| = - (Im a) & - (Im a) <= - (- |.a.|) ) by COMPLEX155a, ABSVALUE:def 1, XREAL_1:24;
hence Im a is light by XXREAL_0:2, Def2; :: thesis: verum

end;

end;