let A, B, C, D be Point of (TOP-REAL 2); :: thesis: ( 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 ; :: thesis: |.(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; :: thesis: verum