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 3
.= 0 by A1, Lm8 ; :: thesis: verum