theorem Th60: :: EUCLID13:71

for A, B, C being Point of (TOP-REAL 2) st A,C,B is_a_triangle & angle (A,C,B) < PI holds
tan (((angle (B,A,C)) - (angle (C,B,A))) / 2) = (cot ((angle (A,C,B)) / 2)) * ((|.(C - B).| - |.(C - A).|) / (|.(C - B).| + |.(C - A).|))