let z be complex number ; :: 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:52, XXREAL_0:1;

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

hence Im z >= 0 by Th36; :: 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 Th27; :: thesis: verum

end;

end;