theorem Th63: :: EUCLID13:75

for A, B, C being Point of (TOP-REAL 2) st A,C,B is_a_triangle & angle (A,C,B) < PI holds
|.(B - C).| = (|.(A - B).| * (sin (angle (B,A,C)))) / (sin ((angle (B,A,C)) + (angle (C,B,A))))