let a, b be Complex; :: thesis: angle (a,b,a) = 0
(Arg (a - b)) - (Arg (a - b)) = 0 ;
hence angle (a,b,a) = 0 by Def4; :: thesis: verum