theorem :: EUCLID13:90

for A, B, C, D being Point of (TOP-REAL 2) st B,C,A is_a_triangle & angle (B,C,A) < PI & D,C,A is_a_triangle & angle (C,D,A) = PI / 2 & A in LSeg (D,B) & A <> D holds
|.(D - C).| = ((|.(A - B).| * (sin (angle (A,B,C)))) / (sin ((angle (D,A,C)) - (angle (A,B,C))))) * (sin (angle (D,A,C)))