let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle & angle (C,A,B) < PI implies ( ((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 ) )
assume that
A1: A,B,C is_a_triangle and
A2: angle (C,A,B) < PI ; :: thesis: ( ((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 )
B,A,C is_a_triangle by A1, MENELAUS:15;
hence ( ((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 ) by A2, Lm11; :: thesis: verum