let A, B, C be Point of (TOP-REAL 2); :: thesis: ( B <> A implies ((sin (((angle (B,A,C)) + (angle (C,B,A))) / 2)) * (cos (((angle (B,A,C)) - (angle (C,B,A))) / 2))) * (|.(C - B).| - |.(C - A).|) = ((sin (((angle (B,A,C)) - (angle (C,B,A))) / 2)) * (cos (((angle (B,A,C)) + (angle (C,B,A))) / 2))) * (|.(C - B).| + |.(C - A).|) )
assume B <> A ; :: thesis: ((sin (((angle (B,A,C)) + (angle (C,B,A))) / 2)) * (cos (((angle (B,A,C)) - (angle (C,B,A))) / 2))) * (|.(C - B).| - |.(C - A).|) = ((sin (((angle (B,A,C)) - (angle (C,B,A))) / 2)) * (cos (((angle (B,A,C)) + (angle (C,B,A))) / 2))) * (|.(C - B).| + |.(C - A).|)
then A1: ((sin (angle (B,A,C))) + (sin (angle (C,B,A)))) * (|.(C - B).| - |.(C - A).|) = ((sin (angle (B,A,C))) - (sin (angle (C,B,A)))) * (|.(C - B).| + |.(C - A).|) by Th57;
set BAC = angle (B,A,C);
set CBA = angle (C,B,A);
(sin (angle (B,A,C))) + (sin (angle (C,B,A))) = 2 * ((cos (((angle (B,A,C)) - (angle (C,B,A))) / 2)) * (sin (((angle (B,A,C)) + (angle (C,B,A))) / 2))) by SIN_COS4:15;
then (2 * ((cos (((angle (B,A,C)) - (angle (C,B,A))) / 2)) * (sin (((angle (B,A,C)) + (angle (C,B,A))) / 2)))) * (|.(C - B).| - |.(C - A).|) = (2 * ((cos (((angle (B,A,C)) + (angle (C,B,A))) / 2)) * (sin (((angle (B,A,C)) - (angle (C,B,A))) / 2)))) * (|.(C - B).| + |.(C - A).|) by A1, SIN_COS4:16;
hence ((sin (((angle (B,A,C)) + (angle (C,B,A))) / 2)) * (cos (((angle (B,A,C)) - (angle (C,B,A))) / 2))) * (|.(C - B).| - |.(C - A).|) = ((sin (((angle (B,A,C)) - (angle (C,B,A))) / 2)) * (cos (((angle (B,A,C)) + (angle (C,B,A))) / 2))) * (|.(C - B).| + |.(C - A).|) ; :: thesis: verum