theorem :: EUCLID13:89

for A, B, C, D being Point of (TOP-REAL 2) st 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 holds
|.(D - C).| = ((|.(A - B).| * (sin (angle (C,B,A)))) / (sin ((angle (C,A,D)) - (angle (C,B,A))))) * (sin (angle (C,A,D)))