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