let A, B be Point of (TOP-REAL 2); :: thesis: angle (A,B,A) = 0
0 = angle ((euc2cpx A),(euc2cpx B),(euc2cpx A)) by COMPLEX2:79
.= angle (A,B,A) by EUCLID_3:def 4 ;
hence angle (A,B,A) = 0 ; :: thesis: verum