theorem Th57: :: EUCLID13:68

for A, B, C being Point of (TOP-REAL 2) st B <> A holds
((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).|)