theorem Th59: :: EUCLID13:70

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