let c1, c2 be Element of COMPLEX ; :: thesis: ( c2 <> 0 & (Arg c2) - (Arg c1) >= 0 implies angle c1,c2 = (Arg c2) - (Arg c1) )
assume that
A1: c2 <> 0 and
A2: (Arg c2) - (Arg c1) >= 0 ; :: thesis: angle c1,c2 = (Arg c2) - (Arg c1)
thus angle c1,c2 = Arg (Rotate c2,(- (Arg c1))) by A1, COMPLEX2:def 5
.= (Arg c2) - (Arg c1) by A1, A2, Lm10 ; :: thesis: verum