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) = ((arctan ((cot ((angle (A,C,B)) / 2)) * ((|.(C - B).| - |.(C - A).|) / (|.(C - B).| + |.(C - A).|)))) + (PI / 2)) - ((angle (A,C,B)) / 2) & angle (C,B,A) = ((PI / 2) - ((angle (A,C,B)) / 2)) - (arctan ((cot ((angle (A,C,B)) / 2)) * ((|.(C - B).| - |.(C - A).|) / (|.(C - B).| + |.(C - A).|)))) ) )
assume ( A,C,B is_a_triangle & angle (A,C,B) < PI ) ; :: thesis: ( angle (B,A,C) = ((arctan ((cot ((angle (A,C,B)) / 2)) * ((|.(C - B).| - |.(C - A).|) / (|.(C - B).| + |.(C - A).|)))) + (PI / 2)) - ((angle (A,C,B)) / 2) & angle (C,B,A) = ((PI / 2) - ((angle (A,C,B)) / 2)) - (arctan ((cot ((angle (A,C,B)) / 2)) * ((|.(C - B).| - |.(C - A).|) / (|.(C - B).| + |.(C - A).|)))) )
then ( (angle (B,A,C)) - (angle (C,B,A)) = 2 * (arctan ((cot ((angle (A,C,B)) / 2)) * ((|.(C - B).| - |.(C - A).|) / (|.(C - B).| + |.(C - A).|)))) & (angle (B,A,C)) + (angle (C,B,A)) = PI - (angle (A,C,B)) ) by Th62, Th24;
hence ( angle (B,A,C) = ((arctan ((cot ((angle (A,C,B)) / 2)) * ((|.(C - B).| - |.(C - A).|) / (|.(C - B).| + |.(C - A).|)))) + (PI / 2)) - ((angle (A,C,B)) / 2) & angle (C,B,A) = ((PI / 2) - ((angle (A,C,B)) / 2)) - (arctan ((cot ((angle (A,C,B)) / 2)) * ((|.(C - B).| - |.(C - A).|) / (|.(C - B).| + |.(C - A).|)))) ) ; :: thesis: verum