let A, B, C be Point of (TOP-REAL 2); :: thesis: ( B <> A implies ((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).|) )
assume B <> A ; :: thesis: ((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).|)
then |.(C - B).| * (sin (angle (C,B,A))) = |.(C - A).| * (sin (angle (B,A,C))) by EUCLID_6:6;
hence ((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).|) ; :: thesis: verum