let A, B, C be Point of (TOP-REAL 2); ( 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
; |.(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)))
;
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)))
;
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; verum