theorem :: EUCLID13:86

for s being Real
for A, B, C, D being Point of (TOP-REAL 2)
for a, b, c, d, R, theta being Real st D <> C & 0 <= R & 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) & R * (cos s) = (sin a) / (sin (a + b)) & R * (sin s) = (sin c) / (sin ((b + d) + c)) & 0 < theta & theta < PI & (sin (2 * s)) * (cos d) = cos (2 * theta) holds
|.(D - C).| = ((|.(A - B).| * (sqrt 2)) * R) * (sin theta)