let a, b be Element of COMPLEX ; :: thesis: angle (a,b) = angle (a,0,b)
set ab2 = angle (a,b);
A1: ( 0 <= Arg (Rotate (b,(- (Arg a)))) & Arg (Rotate (b,(- (Arg a)))) < 2 * PI ) by COMPTRIG:34;

per cases ( b <> 0 or b = 0 ) ;

suppose A2: b <> 0 ; :: thesis: angle (a,b) = angle (a,0,b)

then A3: angle (a,b) = Arg (Rotate (b,(- (Arg a)))) by Def5;
thus angle (a,b) = angle (a,0,b) :: thesis: verum

proof

per cases ( (Arg (b - 0c)) - (Arg (a - 0c)) >= 0 or (Arg (b - 0c)) - (Arg (a - 0c)) < 0 ) ;

suppose (Arg (b - 0c)) - (Arg (a - 0c)) >= 0 ; :: thesis: angle (a,b) = angle (a,0,b)

then A4: angle (a,0c,b) = (- (Arg a)) + (Arg b) by Def6;
A5: angle (a,0c,b) < 2 * PI by Th84;
( ex i being Integer st Arg (Rotate (b,(- (Arg a)))) = ((2 * PI) * i) + ((- (Arg a)) + (Arg b)) & 0 <= angle (a,0c,b) ) by A2, Th68, Th84;
hence angle (a,b) = angle (a,0,b) by A1, A3, A4, A5, Th3; :: thesis: verum

end;

suppose A6: (Arg (b - 0c)) - (Arg (a - 0c)) < 0 ; :: thesis: angle (a,b) = angle (a,0,b)

consider i being Integer such that
A7: Arg (Rotate (b,(- (Arg a)))) = ((2 * PI) * i) + ((- (Arg a)) + (Arg b)) by A2, Th68;
A8: ((2 * PI) * i) + ((- (Arg a)) + (Arg b)) = ((2 * PI) * (i - 1)) + ((2 * PI) + ((- (Arg a)) + (Arg b))) ;
A9: angle (a,0c,b) = (2 * PI) + ((Arg b) + (- (Arg a))) by A6, Def6;
then ( 0 <= (2 * PI) + ((- (Arg a)) + (Arg b)) & (2 * PI) + ((- (Arg a)) + (Arg b)) < 2 * PI ) by Th84;
hence angle (a,b) = angle (a,0,b) by A1, A3, A9, A7, A8, Th3; :: thesis: verum

end;

end;

end;

end;

suppose A10: b = 0 ; :: thesis: angle (a,b) = angle (a,0,b)

thus angle (a,b) = angle (a,0,b) :: thesis: verum

proof

per cases ( Arg a = 0 or Arg a <> 0 ) ;

suppose A11: Arg a = 0 ; :: thesis: angle (a,b) = angle (a,0,b)

then A12: (Arg (b - 0c)) - (Arg (a - 0c)) = 0 by A10, COMPTRIG:35;
angle (a,b) = Arg (Rotate (b,(- (Arg a)))) by A11, Def5
.= 0 by A10, Lm1, Th66 ;
hence angle (a,b) = angle (a,0,b) by A12, Def6; :: thesis: verum

end;

suppose A13: Arg a <> 0 ; :: thesis: angle (a,b) = angle (a,0,b)

then A14: 0 < - (- (Arg a)) by COMPTRIG:34;
(Arg (b - 0c)) - (Arg (a - 0c)) = - (Arg a) by A10, Lm1;
then angle (a,0c,b) = (2 * PI) - (Arg a) by A14, Def6;
hence angle (a,b) = angle (a,0,b) by A10, A13, Def5; :: thesis: verum

end;

end;

end;

end;

end;