theorem :: COMPLEX2:20

for x, y being Complex st Arg x < PI & Arg y < PI holds
Arg (x + y) < PI