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 & A in LSeg (B,D) & A <> D implies |.(D - C).| = ((|.(A - B).| * (sin (angle (C,B,A)))) / (sin ((angle (C,A,D)) - (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 and
A5: A in LSeg (B,D) and
A6: A <> D ; :: thesis: |.(D - C).| = ((|.(A - B).| * (sin (angle (C,B,A)))) / (sin ((angle (C,A,D)) - (angle (C,B,A))))) * (sin (angle (C,A,D)))
A,C,B are_mutually_distinct by A1, EUCLID_6:20;
then ( (angle (B,A,C)) + (angle (C,A,D)) = PI or (angle (B,A,C)) + (angle (C,A,D)) = 3 * PI ) by A5, A6, EUCLID_6:13;
then ( sin ((angle (B,A,C)) + (angle (C,B,A))) = sin (PI - ((angle (C,A,D)) - (angle (C,B,A)))) or sin ((angle (B,A,C)) + (angle (C,B,A))) = sin (((2 * PI) * 1) + (PI - ((angle (C,A,D)) - (angle (C,B,A))))) ) ;
then ( sin ((angle (B,A,C)) + (angle (C,B,A))) = sin (PI - ((angle (C,A,D)) - (angle (C,B,A)))) or sin ((angle (B,A,C)) + (angle (C,B,A))) = sin (PI - ((angle (C,A,D)) - (angle (C,B,A)))) ) by COMPLEX2:8;
then sin ((angle (B,A,C)) + (angle (C,B,A))) = sin ((angle (C,A,D)) - (angle (C,B,A))) by EUCLID10:1;
hence |.(D - C).| = ((|.(A - B).| * (sin (angle (C,B,A)))) / (sin ((angle (C,A,D)) - (angle (C,B,A))))) * (sin (angle (C,A,D))) by A1, A2, A3, A4, Th70; :: thesis: verum