let A, B, C, D be 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)))
let a, b, c, d be Real; ( 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) implies |.(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))) )
assume that
A1:
A,C,B is_a_triangle
and
A2:
angle (A,C,B) < PI
and
A3:
A,D,B is_a_triangle
and
A4:
angle (A,D,B) < PI
and
A5:
( a = angle (C,B,A) & b = angle (B,A,C) & c = angle (D,B,A) & d = angle (C,A,D) )
; |.(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)))
set e = b + d;
A6:
( b + d = angle (B,A,D) or b + d = (angle (B,A,D)) + (2 * PI) )
by A5, EUCLID_6:4;
A7:
sin ((b + d) + c) = sin ((angle (B,A,D)) + (angle (D,B,A)))
A8: |.(C - A).| =
|.(A - C).|
by EUCLID_6:43
.=
(|.(A - B).| * (sin (angle (C,B,A)))) / (sin ((angle (B,A,C)) + (angle (C,B,A))))
by A1, A2, Th64
;
then A9: |.(C - A).| ^2 =
(|.(A - B).| * ((sin (angle (C,B,A))) / (sin ((angle (B,A,C)) + (angle (C,B,A)))))) ^2
.=
(|.(A - B).| ^2) * (((sin (angle (C,B,A))) / (sin ((angle (B,A,C)) + (angle (C,B,A))))) ^2)
by SQUARE_1:9
;
A10: |.(D - A).| =
|.(A - D).|
by EUCLID_6:43
.=
(|.(A - B).| * (sin (angle (D,B,A)))) / (sin ((angle (B,A,D)) + (angle (D,B,A))))
by A3, A4, Th64
;
then A11: |.(D - A).| ^2 =
(|.(A - B).| * ((sin (angle (D,B,A))) / (sin ((angle (B,A,D)) + (angle (D,B,A)))))) ^2
.=
(|.(A - B).| ^2) * (((sin (angle (D,B,A))) / (sin ((angle (B,A,D)) + (angle (D,B,A))))) ^2)
by SQUARE_1:9
;
|.(D - C).| ^2 =
(((|.(A - B).| ^2) * (((sin (angle (C,B,A))) / (sin ((angle (B,A,C)) + (angle (C,B,A))))) ^2)) + ((|.(A - B).| ^2) * (((sin (angle (D,B,A))) / (sin ((angle (B,A,D)) + (angle (D,B,A))))) ^2))) - (((2 * ((|.(A - B).| * (sin (angle (C,B,A)))) / (sin ((angle (B,A,C)) + (angle (C,B,A)))))) * ((|.(A - B).| * (sin (angle (D,B,A)))) / (sin ((angle (B,A,D)) + (angle (D,B,A)))))) * (cos (angle (C,A,D))))
by A8, A9, A10, A11, EUCLID_6:7
.=
(((|.(A - B).| ^2) * (((sin (angle (C,B,A))) / (sin ((angle (B,A,C)) + (angle (C,B,A))))) ^2)) + ((|.(A - B).| ^2) * (((sin (angle (D,B,A))) / (sin ((angle (B,A,D)) + (angle (D,B,A))))) ^2))) - ((((2 * (((|.(A - B).| * |.(A - B).|) * (sin (angle (C,B,A)))) / (sin ((angle (B,A,C)) + (angle (C,B,A)))))) * (sin (angle (D,B,A)))) / (sin ((angle (B,A,D)) + (angle (D,B,A))))) * (cos (angle (C,A,D))))
.=
(((|.(A - B).| ^2) * (((sin (angle (C,B,A))) / (sin ((angle (B,A,C)) + (angle (C,B,A))))) ^2)) + ((|.(A - B).| ^2) * (((sin (angle (D,B,A))) / (sin ((angle (B,A,D)) + (angle (D,B,A))))) ^2))) - ((((2 * (((|.(A - B).| ^2) * (sin (angle (C,B,A)))) / (sin ((angle (B,A,C)) + (angle (C,B,A)))))) * (sin (angle (D,B,A)))) / (sin ((angle (B,A,D)) + (angle (D,B,A))))) * (cos (angle (C,A,D))))
by SQUARE_1:def 1
.=
(|.(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)))
by A5, A7
;
hence
|.(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)))
; verum