let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle & angle (C,B,A) < PI implies (((angle (C,B,A)) / 3) + ((angle (B,A,C)) / 3)) + ((angle (A,C,B)) / 3) = PI / 3 )
assume that
A1: A,B,C is_a_triangle and
A2: angle (C,B,A) < PI ; :: thesis: (((angle (C,B,A)) / 3) + ((angle (B,A,C)) / 3)) + ((angle (A,C,B)) / 3) = PI / 3
((angle (C,B,A)) + (angle (B,A,C))) + (angle (A,C,B)) = PI by A1, A2, Lm11;
hence (((angle (C,B,A)) / 3) + ((angle (B,A,C)) / 3)) + ((angle (A,C,B)) / 3) = PI / 3 ; :: thesis: verum