let a, b be Element of COMPLEX ; :: thesis: angle a,b,a = 0
(Arg (a - b)) - (Arg (a - b)) = 0 ;
hence angle a,b,a = 0 by Def6; :: thesis: verum