theorem :: EUCLID10:54

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