let A, B, C be Point of (TOP-REAL 2); :: thesis: ( 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 ; :: thesis: ((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; :: thesis: verum