let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,C,B is_a_triangle & angle (A,C,B) < PI implies (angle (B,A,C)) + (angle (C,B,A)) = PI - (angle (A,C,B)) )
assume ( A,C,B is_a_triangle & angle (A,C,B) < PI ) ; :: thesis: (angle (B,A,C)) + (angle (C,B,A)) = PI - (angle (A,C,B))
then angle (A,C,B) = PI - ((angle (C,B,A)) + (angle (B,A,C))) by Th23;
hence (angle (B,A,C)) + (angle (C,B,A)) = PI - (angle (A,C,B)) ; :: thesis: verum