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

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

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

end;

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

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

end;

end;