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