theorem Th15: :: COMPLEX2:17

for x, y being Complex st ( x <> y or x - y <> 0 ) holds
( Arg (x - y) < PI iff Arg (y - x) >= PI )