theorem :: EUCLID_3:29

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