let z be complex number ; :: thesis: ( Im z >= 0 implies sin (Arg z) >= 0 )
assume Im z >= 0 ; :: thesis: sin (Arg z) >= 0
then ( Im z > 0 or Im z = 0 ) ;
then ( sin (Arg z) > 0 or ( z = (Re z) + (0 * <i> ) & ( Re z >= 0 or Re z < 0 ) ) ) by Th63, COMPLEX1:29;
hence sin (Arg z) >= 0 by Th53, Th54, SIN_COS:34, SIN_COS:82; :: thesis: verum