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