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

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

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

end;

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

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

end;

end;