let A, B, C be Point of (TOP-REAL 2); ( 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
; ( - 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 )
; verum