let s be 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)
let A, B, C, D be 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 Real; 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; ( 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)
; |.(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))
hence
|.(D - C).| = ((|.(A - B).| * (sqrt 2)) * R) * (sin theta)
by A10, A8, SQUARE_1:40; verum