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

proof

(|.(A - B).| * (sin (angle (C,B,A)))) / (sin (angle (A,C,B))) = (|.(A - C).| * (sin (angle (A,C,B)))) / (sin (angle (A,C,B))) by A3, EUCLID_6:6
.= |.(A - C).| * ((sin (angle (A,C,B))) / (sin (angle (A,C,B))))
.= |.(A - C).| * 1 by A1, Th22, XCMPLX_1:60
.= |.(A - C).| ;
hence |.(A - C).| = (|.(A - B).| * (sin (angle (C,B,A)))) / (sin (angle (A,C,B))) ; :: thesis: verum

end;

angle (A,C,B) = PI - ((angle (C,B,A)) + (angle (B,A,C)))

proof

A,C,B are_mutually_distinct by A1, EUCLID_6:20;
then ((angle (A,C,B)) + (angle (C,B,A))) + (angle (B,A,C)) = PI by A2, EUCLID_3:47;
hence angle (A,C,B) = PI - ((angle (C,B,A)) + (angle (B,A,C))) ; :: thesis: verum

end;

hence |.(A - C).| = (|.(A - B).| * (sin (angle (C,B,A)))) / (sin ((angle (B,A,C)) + (angle (C,B,A)))) by A4, EUCLID10:1; :: thesis: verum