let z be Complex; :: thesis: ( Arg z <= PI implies Im z >= 0 )
assume A1: Arg z <= PI ; :: thesis: Im z >= 0

per cases ( Arg z = PI or Arg z = 0 or ( 0 < Arg z & Arg z < PI ) ) by A1, COMPTRIG:34, XXREAL_0:1;

suppose ( Arg z = PI or Arg z = 0 ) ; :: thesis: Im z >= 0

hence Im z >= 0 by Th21; :: thesis: verum

end;

suppose ( 0 < Arg z & Arg z < PI ) ; :: thesis: Im z >= 0

then Arg z in ].0,PI.[ by XXREAL_1:4;
hence Im z >= 0 by Th16; :: thesis: verum

end;

end;