let A, B, C be Point of (TOP-REAL 2); ( A,C,B is_a_triangle & angle (A,C,B) < PI implies ((angle (B,A,C)) - (angle (C,B,A))) / 2 = arctan ((cot ((angle (A,C,B)) / 2)) * ((|.(C - B).| - |.(C - A).|) / (|.(C - B).| + |.(C - A).|))) )
assume that
A1:
A,C,B is_a_triangle
and
A2:
angle (A,C,B) < PI
; ((angle (B,A,C)) - (angle (C,B,A))) / 2 = arctan ((cot ((angle (A,C,B)) / 2)) * ((|.(C - B).| - |.(C - A).|) / (|.(C - B).| + |.(C - A).|)))
set r = ((angle (B,A,C)) - (angle (C,B,A))) / 2;
A3:
tan (((angle (B,A,C)) - (angle (C,B,A))) / 2) = (cot ((angle (A,C,B)) / 2)) * ((|.(C - B).| - |.(C - A).|) / (|.(C - B).| + |.(C - A).|))
by A1, A2, Th60;
0 <= angle (A,C,B)
by EUCLID11:2;
then A4:
( 0 < angle (A,C,B) & angle (A,C,B) < PI & A,C,B are_mutually_distinct )
by A1, A2, EUCLID10:30, EUCLID_6:20;
( 0 < angle (B,A,C) & angle (B,A,C) < PI & A,B,C is_a_triangle )
by A4, EUCLID11:5, A1, MENELAUS:15;
then
( - (PI / 2) < ((angle (B,A,C)) - (angle (C,B,A))) / 2 & ((angle (B,A,C)) - (angle (C,B,A))) / 2 < PI / 2 )
by Th29;
hence
((angle (B,A,C)) - (angle (C,B,A))) / 2 = arctan ((cot ((angle (A,C,B)) / 2)) * ((|.(C - B).| - |.(C - A).|) / (|.(C - B).| + |.(C - A).|)))
by A3, SIN_COS9:35; verum