theorem :: EUCLID_3:32

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