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

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

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

end;

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

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

end;

end;