let c1, c2, c3 be Element of COMPLEX ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

per cases ( ( c2 = 0 & c3 = 0 ) or ( c2 <> 0 & c3 = 0 ) or ( c2 = 0 & c3 <> 0 ) or ( c2 <> 0 & c3 <> 0 ) ) ;

suppose A1: ( c2 = 0 & c3 = 0 ) ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

then A2: Arg c2 = 0 by COMPTRIG:def 1;

per cases ( Arg c1 = 0 or Arg c1 <> 0 ) ;

suppose Arg c1 = 0 ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

then (angle (c1,c2)) + (angle (c2,c3)) = 0 + (angle (c2,c3)) by A1, Lm9;
hence ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) ) by A1, A2, Lm9; :: thesis: verum

end;

suppose A3: Arg c1 <> 0 ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

then (angle (c1,c2)) + (angle (c2,c3)) = ((2 * PI) - (Arg c1)) + (angle (c2,c3)) by A1, COMPLEX2:def 3
.= ((2 * PI) - (Arg c1)) + 0 by A1, A2, Lm9 ;
hence ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) ) by A1, A3, COMPLEX2:def 3; :: thesis: verum

end;

end;

end;

suppose A4: ( c2 <> 0 & c3 = 0 ) ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

per cases ( ( Arg c1 = 0 & Arg c2 = 0 ) or ( Arg c1 <> 0 & Arg c2 = 0 ) or ( Arg c1 = 0 & Arg c2 <> 0 ) or ( Arg c1 <> 0 & Arg c2 <> 0 ) ) ;

suppose A5: ( Arg c1 = 0 & Arg c2 = 0 ) ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

per cases ( (Arg c2) - (Arg c1) < 0 or (Arg c2) - (Arg c1) >= 0 ) ;

suppose (Arg c2) - (Arg c1) < 0 ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

hence ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) ) by A5; :: thesis: verum

end;

suppose (Arg c2) - (Arg c1) >= 0 ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

then (angle (c1,c2)) + (angle (c2,c3)) = ((Arg c2) - (Arg c1)) + (angle (c2,c3)) by A4, Lm11
.= 0 by A4, A5, Lm9 ;
hence ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) ) by A4, A5, Lm9; :: thesis: verum

end;

end;

end;

suppose A6: ( Arg c1 <> 0 & Arg c2 = 0 ) ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

per cases ( (Arg c2) - (Arg c1) < 0 or (Arg c2) - (Arg c1) >= 0 ) ;

suppose (Arg c2) - (Arg c1) < 0 ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

then (angle (c1,c2)) + (angle (c2,c3)) = (((2 * PI) - (Arg c1)) + (Arg c2)) + (angle (c2,c3)) by A4, Lm13
.= (2 * PI) - (Arg c1) by A4, A6, Lm9 ;
hence ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) ) by A4, A6, COMPLEX2:def 3; :: thesis: verum

end;

suppose (Arg c2) - (Arg c1) >= 0 ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

then - (- (Arg c1)) <= - 0 by A6;
hence ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) ) by A6, COMPTRIG:34; :: thesis: verum

end;

end;

end;

suppose A7: ( Arg c1 = 0 & Arg c2 <> 0 ) ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

per cases ( (Arg c2) - (Arg c1) < 0 or (Arg c2) - (Arg c1) >= 0 ) ;

suppose (Arg c2) - (Arg c1) < 0 ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

hence ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) ) by A7, COMPTRIG:34; :: thesis: verum

end;

suppose A8: (Arg c2) - (Arg c1) >= 0 ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

A9: angle (c1,c3) = 0 by A4, A7, Lm9;
(angle (c1,c2)) + (angle (c2,c3)) = ((Arg c2) - (Arg c1)) + (angle (c2,c3)) by A4, A8, Lm11
.= (Arg c2) + ((2 * PI) - (Arg c2)) by A4, A7, COMPLEX2:def 3 ;
hence ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) ) by A9; :: thesis: verum

end;

end;

end;

suppose A10: ( Arg c1 <> 0 & Arg c2 <> 0 ) ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

per cases ( (Arg c2) - (Arg c1) < 0 or (Arg c2) - (Arg c1) >= 0 ) ;

suppose A11: (Arg c2) - (Arg c1) < 0 ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

A12: angle (c1,c3) = (2 * PI) - (Arg c1) by A4, A10, COMPLEX2:def 3;
(angle (c1,c2)) + (angle (c2,c3)) = (((2 * PI) - (Arg c1)) + (Arg c2)) + (angle (c2,c3)) by A4, A11, Lm13
.= (((2 * PI) - (Arg c1)) + (Arg c2)) + ((2 * PI) - (Arg c2)) by A4, A10, COMPLEX2:def 3
.= ((2 * PI) + (2 * PI)) - (Arg c1) ;
hence ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) ) by A12; :: thesis: verum

end;

suppose A13: (Arg c2) - (Arg c1) >= 0 ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

A14: angle (c1,c3) = (2 * PI) - (Arg c1) by A4, A10, COMPLEX2:def 3;
(angle (c1,c2)) + (angle (c2,c3)) = ((Arg c2) - (Arg c1)) + (angle (c2,c3)) by A4, A13, Lm11
.= ((Arg c2) - (Arg c1)) + ((2 * PI) - (Arg c2)) by A4, A10, COMPLEX2:def 3 ;
hence ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) ) by A14; :: thesis: verum

end;

end;

end;

end;

end;

suppose A15: ( c2 = 0 & c3 <> 0 ) ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

per cases ( ( (Arg c3) - (Arg c2) < 0 & (Arg c3) - (Arg c1) < 0 ) or ( (Arg c3) - (Arg c2) >= 0 & (Arg c3) - (Arg c1) < 0 ) or ( (Arg c3) - (Arg c2) < 0 & (Arg c3) - (Arg c1) >= 0 ) or ( (Arg c3) - (Arg c2) >= 0 & (Arg c3) - (Arg c1) >= 0 ) ) ;

suppose ( (Arg c3) - (Arg c2) < 0 & (Arg c3) - (Arg c1) < 0 ) ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

then (Arg c3) - 0 < 0 by A15, COMPTRIG:def 1;
hence ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) ) by COMPTRIG:34; :: thesis: verum

end;

suppose A16: ( (Arg c3) - (Arg c2) >= 0 & (Arg c3) - (Arg c1) < 0 ) ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

per cases ( Arg c1 = 0 or Arg c1 <> 0 ) ;

suppose Arg c1 = 0 ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

hence ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) ) by A16, COMPTRIG:34; :: thesis: verum

end;

suppose Arg c1 <> 0 ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

then (angle (c1,c2)) + (angle (c2,c3)) = ((2 * PI) - (Arg c1)) + (angle (c2,c3)) by A15, COMPLEX2:def 3
.= ((2 * PI) - (Arg c1)) + ((Arg c3) - (Arg c2)) by A15, A16, Lm11
.= ((2 * PI) - (Arg c1)) + ((Arg c3) - 0) by A15, COMPTRIG:def 1
.= ((2 * PI) - (Arg c1)) + (Arg c3) ;
hence ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) ) by A15, A16, Lm13; :: thesis: verum

end;

end;

end;

suppose ( (Arg c3) - (Arg c2) < 0 & (Arg c3) - (Arg c1) >= 0 ) ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

then (Arg c3) - 0 < 0 by A15, COMPTRIG:def 1;
hence ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) ) by COMPTRIG:34; :: thesis: verum

end;

suppose A17: ( (Arg c3) - (Arg c2) >= 0 & (Arg c3) - (Arg c1) >= 0 ) ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

per cases ( Arg c1 = 0 or Arg c1 <> 0 ) ;

suppose A18: Arg c1 = 0 ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

then (angle (c1,c2)) + (angle (c2,c3)) = 0 + (angle (c2,c3)) by A15, Lm9
.= 0 + ((Arg c3) - (Arg c2)) by A15, A17, Lm11
.= 0 + ((Arg c3) - 0) by A15, COMPTRIG:def 1 ;
hence ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) ) by A15, A17, A18, Lm11; :: thesis: verum

end;

suppose A19: Arg c1 <> 0 ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

A20: angle (c1,c3) = (Arg c3) - (Arg c1) by A15, A17, Lm11;
(angle (c1,c2)) + (angle (c2,c3)) = ((2 * PI) - (Arg c1)) + (angle (c2,c3)) by A15, A19, COMPLEX2:def 3
.= ((2 * PI) - (Arg c1)) + ((Arg c3) - (Arg c2)) by A15, A17, Lm11
.= ((2 * PI) - (Arg c1)) + ((Arg c3) - 0) by A15, COMPTRIG:def 1 ;
hence ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) ) by A20; :: thesis: verum

end;

end;

end;

end;

end;

suppose A21: ( c2 <> 0 & c3 <> 0 ) ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

per cases ( ( (Arg c3) - (Arg c2) < 0 & (Arg c3) - (Arg c1) < 0 ) or ( (Arg c3) - (Arg c2) >= 0 & (Arg c3) - (Arg c1) < 0 ) or ( (Arg c3) - (Arg c2) < 0 & (Arg c3) - (Arg c1) >= 0 ) or ( (Arg c3) - (Arg c2) >= 0 & (Arg c3) - (Arg c1) >= 0 ) ) ;

suppose A22: ( (Arg c3) - (Arg c2) < 0 & (Arg c3) - (Arg c1) < 0 ) ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

per cases ( (Arg c2) - (Arg c1) < 0 or (Arg c2) - (Arg c1) >= 0 ) ;

suppose A23: (Arg c2) - (Arg c1) < 0 ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

A24: angle (c1,c3) = ((2 * PI) - (Arg c1)) + (Arg c3) by A21, A22, Lm13;
(angle (c1,c2)) + (angle (c2,c3)) = (((2 * PI) - (Arg c1)) + (Arg c2)) + (angle (c2,c3)) by A21, A23, Lm13
.= (((2 * PI) - (Arg c1)) + (Arg c2)) + (((2 * PI) - (Arg c2)) + (Arg c3)) by A21, A22, Lm13
.= (((2 * PI) + (2 * PI)) - (Arg c1)) + (Arg c3) ;
hence ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) ) by A24; :: thesis: verum

end;

suppose (Arg c2) - (Arg c1) >= 0 ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

then (angle (c1,c2)) + (angle (c2,c3)) = ((Arg c2) - (Arg c1)) + (angle (c2,c3)) by A21, Lm11
.= ((Arg c2) - (Arg c1)) + (((2 * PI) - (Arg c2)) + (Arg c3)) by A21, A22, Lm13
.= ((2 * PI) - (Arg c1)) + (Arg c3) ;
hence ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) ) by A21, A22, Lm13; :: thesis: verum

end;

end;

end;

suppose A25: ( (Arg c3) - (Arg c2) >= 0 & (Arg c3) - (Arg c1) < 0 ) ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

per cases ( (Arg c2) - (Arg c1) < 0 or (Arg c2) - (Arg c1) >= 0 ) ;

suppose (Arg c2) - (Arg c1) < 0 ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

then (angle (c1,c2)) + (angle (c2,c3)) = (((2 * PI) - (Arg c1)) + (Arg c2)) + (angle (c2,c3)) by A21, Lm13
.= (((2 * PI) - (Arg c1)) + (Arg c2)) + ((Arg c3) - (Arg c2)) by A21, A25, Lm11
.= ((2 * PI) - (Arg c1)) + (Arg c3) ;
hence ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) ) by A21, A25, Lm13; :: thesis: verum

end;

suppose (Arg c2) - (Arg c1) >= 0 ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

then ((Arg c2) - (Arg c1)) + ((Arg c3) - (Arg c2)) >= 0 + 0 by A25;
hence ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) ) by A25; :: thesis: verum

end;

end;

end;

suppose A26: ( (Arg c3) - (Arg c2) < 0 & (Arg c3) - (Arg c1) >= 0 ) ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

per cases ( (Arg c2) - (Arg c1) < 0 or (Arg c2) - (Arg c1) >= 0 ) ;

suppose (Arg c2) - (Arg c1) < 0 ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

then ((Arg c2) - (Arg c1)) + ((Arg c3) - (Arg c2)) < 0 + 0 by A26;
hence ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) ) by A26; :: thesis: verum

end;

suppose A27: (Arg c2) - (Arg c1) >= 0 ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

A28: angle (c1,c3) = (Arg c3) - (Arg c1) by A21, A26, Lm11;
(angle (c1,c2)) + (angle (c2,c3)) = ((Arg c2) - (Arg c1)) + (angle (c2,c3)) by A21, A27, Lm11
.= ((Arg c2) - (Arg c1)) + (((2 * PI) - (Arg c2)) + (Arg c3)) by A21, A26, Lm13
.= ((2 * PI) - (Arg c1)) + (Arg c3) ;
hence ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) ) by A28; :: thesis: verum

end;

end;

end;

suppose A29: ( (Arg c3) - (Arg c2) >= 0 & (Arg c3) - (Arg c1) >= 0 ) ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

per cases ( (Arg c2) - (Arg c1) < 0 or (Arg c2) - (Arg c1) >= 0 ) ;

suppose A30: (Arg c2) - (Arg c1) < 0 ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

A31: angle (c1,c3) = (Arg c3) - (Arg c1) by A21, A29, Lm11;
(angle (c1,c2)) + (angle (c2,c3)) = (((2 * PI) - (Arg c1)) + (Arg c2)) + (angle (c2,c3)) by A21, A30, Lm13
.= (((2 * PI) + (Arg c2)) - (Arg c1)) + ((Arg c3) - (Arg c2)) by A21, A29, Lm11
.= ((2 * PI) - (Arg c1)) + (Arg c3) ;
hence ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) ) by A31; :: thesis: verum

end;

suppose (Arg c2) - (Arg c1) >= 0 ; :: thesis: ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) )

then (angle (c1,c2)) + (angle (c2,c3)) = ((Arg c2) - (Arg c1)) + (angle (c2,c3)) by A21, Lm11
.= ((Arg c2) - (Arg c1)) + ((Arg c3) - (Arg c2)) by A21, A29, Lm11
.= (- (Arg c1)) + (Arg c3) ;
hence ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) ) by A21, A29, Lm11; :: thesis: verum

end;

end;

end;

end;

end;

end;