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