let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle implies ( - PI < ((angle (B,A,C)) - (angle (C,B,A))) / 2 & ((angle (B,A,C)) - (angle (C,B,A))) / 2 < PI ) )
assume A,B,C is_a_triangle ; :: thesis: ( - PI < ((angle (B,A,C)) - (angle (C,B,A))) / 2 & ((angle (B,A,C)) - (angle (C,B,A))) / 2 < PI )
then ( (- 2) * PI < (angle (B,A,C)) - (angle (C,B,A)) & (angle (B,A,C)) - (angle (C,B,A)) < 2 * PI ) by Th27;
then ( ((- 2) * PI) / 2 < ((angle (B,A,C)) - (angle (C,B,A))) / 2 & ((angle (B,A,C)) - (angle (C,B,A))) / 2 < (2 * PI) / 2 ) by XREAL_1:74;
hence ( - PI < ((angle (B,A,C)) - (angle (C,B,A))) / 2 & ((angle (B,A,C)) - (angle (C,B,A))) / 2 < PI ) ; :: thesis: verum