for z being Complex st Arg z <> 0 holds
( Arg z < PI iff sin (Arg z) > 0 )