let z be Complex; :: 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 Th45, COMPLEX1:13;
hence sin (Arg z) >= 0 by Th35, Th36, SIN_COS:31, SIN_COS:77; :: thesis: verum