theorem :: EUCLID11:3

for A, B, C being Point of (TOP-REAL 2) holds
( ( 0 <= angle (A,B,C) & angle (A,B,C) < PI ) or angle (A,B,C) = PI or ( PI < angle (A,B,C) & angle (A,B,C) < 2 * PI ) )