let A, B, C be Point of (TOP-REAL 2); :: thesis: ( 0 <= angle (A,B,C) & angle (A,B,C) < 2 * PI )
angle (A,B,C) = angle ((euc2cpx A),(euc2cpx B),(euc2cpx C)) by EUCLID_3:def 4;
hence ( 0 <= angle (A,B,C) & angle (A,B,C) < 2 * PI ) by COMPLEX2:70; :: thesis: verum