theorem Th31: :: EUCLID_3:31

for p being Point of (TOP-REAL 2) st p <> 0. (TOP-REAL 2) holds
( Arg p < PI iff Arg (- p) >= PI )