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;