let c1, c2 be Element of COMPLEX ; :: thesis: ( c2 <> 0 & (Arg c2) - (Arg c1) < 0 implies angle c1,c2 = ((2 * PI ) - (Arg c1)) + (Arg c2) )
assume A1: ( c2 <> 0 & (Arg c2) - (Arg c1) < 0 ) ; :: thesis: angle c1,c2 = ((2 * PI ) - (Arg c1)) + (Arg c2)
hence angle c1,c2 = Arg (Rotate c2,(- (Arg c1))) by COMPLEX2:def 5
.= ((2 * PI ) - (Arg c1)) + (Arg c2) by A1, Lm12 ;
:: thesis: verum