theorem Th27: :: EUCLID13:33

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