let A, B, C, D be Point of (TOP-REAL 2); ( B,C,A is_a_triangle & angle (B,C,A) < PI & D,C,A is_a_triangle & angle (C,D,A) = PI / 2 implies |.(D - C).| = ((|.(A - B).| * (sin (angle (A,B,C)))) / (sin ((angle (A,B,C)) + (angle (C,A,B))))) * (sin (angle (D,A,C))) )
assume that
A1:
B,C,A is_a_triangle
and
A2:
angle (B,C,A) < PI
and
A3:
D,C,A is_a_triangle
and
A4:
angle (C,D,A) = PI / 2
; |.(D - C).| = ((|.(A - B).| * (sin (angle (A,B,C)))) / (sin ((angle (A,B,C)) + (angle (C,A,B))))) * (sin (angle (D,A,C)))
|.(D - C).| =
|.(A - C).| * (sin (angle (D,A,C)))
by A3, A4, EUCLID10:34
.=
((|.(B - A).| * (sin (angle (A,B,C)))) / (sin ((angle (A,B,C)) + (angle (C,A,B))))) * (sin (angle (D,A,C)))
by A1, A2, Th63
;
hence
|.(D - C).| = ((|.(A - B).| * (sin (angle (A,B,C)))) / (sin ((angle (A,B,C)) + (angle (C,A,B))))) * (sin (angle (D,A,C)))
by EUCLID_6:43; verum