let s be Real; :: thesis: 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)
let A, B, C, D be Point of (TOP-REAL 2); :: thesis: 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)
let a, b, c, d be Real; :: thesis: for 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)
let R, theta be Real; :: thesis: ( 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) implies |.(D - C).| = ((|.(A - B).| * (sqrt 2)) * R) * (sin theta) )
assume that
A1: D <> C and
A2: 0 <= R and
A3: ( 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) ) and
A4: R * (cos s) = (sin a) / (sin (a + b)) and
A5: R * (sin s) = (sin c) / (sin ((b + d) + c)) and
A6: ( 0 < theta & theta < PI ) and
A7: (sin (2 * s)) * (cos d) = cos (2 * theta) ; :: thesis: |.(D - C).| = ((|.(A - B).| * (sqrt 2)) * R) * (sin theta)
A8: |.(D - C).| ^2 = (|.(A - B).| ^2) * ((((R * (cos s)) ^2) + ((R * (sin s)) ^2)) - (((2 * (R * (cos s))) * (R * (sin s))) * (cos d))) by A3, A4, A5, Th68
.= (|.(A - B).| ^2) * ((2 * (R ^2)) * ((sin theta) ^2)) by A7, Th69 ;
A9: ( 0 < 2 & sqrt (2 * 2) = 2 ) by SQUARE_1:20;
A10: (|.(A - B).| ^2) * ((2 * (R ^2)) * ((sin theta) ^2)) = (|.(A - B).| * |.(A - B).|) * ((2 * (R ^2)) * ((sin theta) ^2)) by SQUARE_1:def 1
.= (|.(A - B).| * |.(A - B).|) * ((((sqrt 2) * (sqrt 2)) * (R ^2)) * ((sin theta) ^2)) by A9, SQUARE_1:29
.= (|.(A - B).| * |.(A - B).|) * ((((sqrt 2) * (sqrt 2)) * (R * R)) * ((sin theta) ^2)) by SQUARE_1:def 1
.= (|.(A - B).| * |.(A - B).|) * ((((sqrt 2) * (sqrt 2)) * (R * R)) * ((sin theta) * (sin theta))) by SQUARE_1:def 1
.= (((|.(A - B).| * (sqrt 2)) * R) * (sin theta)) * (((|.(A - B).| * (sqrt 2)) * R) * (sin theta))
.= (((|.(A - B).| * (sqrt 2)) * R) * (sin theta)) ^2 by SQUARE_1:def 1 ;
( (2 * PI) * 0 < theta & theta < ((2 * PI) * 0) + PI ) by A6;
then A11: 0 < sin theta by SIN_COS6:11;
not |.(D - C).| = - (((|.(A - B).| * (sqrt 2)) * R) * (sin theta))

proof

assume A12: |.(D - C).| = - (((|.(A - B).| * (sqrt 2)) * R) * (sin theta)) ; :: thesis: contradiction
0 < sqrt 2 by SQUARE_1:25;
then |.(D - C).| = 0 by A12, A2, A11;
hence contradiction by A1, EUCLID_6:42; :: thesis: verum

end;

hence |.(D - C).| = ((|.(A - B).| * (sqrt 2)) * R) * (sin theta) by A10, A8, SQUARE_1:40; :: thesis: verum