theorem Th23: :: EUCLID13:29

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