theorem :: COMPTRIG:52

for z being Complex st Re z <= 0 & z <> 0 holds
cos (Arg z) <= 0