theorem Th29: :: EUCLID13:36

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle & angle (B,A,C) < PI holds
( - (PI / 2) < ((angle (B,A,C)) - (angle (C,B,A))) / 2 & ((angle (B,A,C)) - (angle (C,B,A))) / 2 < PI / 2 )