theorem :: COMPTRIG:51

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