let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( Arg p1 < PI & Arg p2 < PI implies Arg (p1 + p2) < PI )
assume ( Arg p1 < PI & Arg p2 < PI ) ; :: thesis: Arg (p1 + p2) < PI
then Arg ((euc2cpx p1) + (euc2cpx p2)) < PI by COMPLEX2:20;
hence Arg (p1 + p2) < PI by Th9; :: thesis: verum