theorem :: COMPTRIG:48

for z being Complex st Im z <= 0 holds
sin (Arg z) <= 0