theorem :: EUCLID_3:34

for p1, p2 being Point of (TOP-REAL 2) st Arg p1 < PI & Arg p2 < PI holds
Arg (p1 + p2) < PI