theorem Th58: :: EUCLID13:69

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