theorem Th68: :: EUCLID13:84

for A, B, C, D being Point of (TOP-REAL 2)
for a, b, c, d being Real st A,C,B is_a_triangle & angle (A,C,B) < PI & A,D,B is_a_triangle & angle (A,D,B) < PI & a = angle (C,B,A) & b = angle (B,A,C) & c = angle (D,B,A) & d = angle (C,A,D) holds
|.(D - C).| ^2 = (|.(A - B).| ^2) * (((((sin a) / (sin (a + b))) ^2) + (((sin c) / (sin ((b + d) + c))) ^2)) - (((2 * ((sin a) / (sin (b + a)))) * ((sin c) / (sin ((b + d) + c)))) * (cos d)))