let A, B, C be Point of (TOP-REAL 2); ( A,B,C is_a_triangle implies |.(A - B).| = (the_diameter_of_the_circumcircle (A,B,C)) * (sin (angle (A,C,B))) )
assume
A,B,C is_a_triangle
; |.(A - B).| = (the_diameter_of_the_circumcircle (A,B,C)) * (sin (angle (A,C,B)))
then A2:
the_area_of_polygon3 (A,B,C) <> 0
by MENELAUS:9;
set k = ((|.(A - B).| * |.(B - C).|) * |.(C - A).|) / (the_area_of_polygon3 (B,C,A));
A3:
the_area_of_polygon3 (B,C,A) = ((|.(B - C).| * |.(A - C).|) * (sin (angle (A,C,B)))) / 2
by EUCLID_6:5;
the_area_of_polygon3 (B,C,A) <> 0
by A2, Thm27;
then A4:
|.(A - B).| = (|.(A - B).| * (the_area_of_polygon3 (B,C,A))) / (the_area_of_polygon3 (B,C,A))
by XCMPLX_1:89;
A5:
|.(A - B).| = ((((|.(A - B).| * |.(B - C).|) * |.(A - C).|) * (sin (angle (A,C,B)))) / 2) / (the_area_of_polygon3 (B,C,A))
by A4, A3;
set abc = (|.(A - B).| * |.(B - C).|) * |.(C - A).|;
set S = the_area_of_polygon3 (B,C,A);
set an = sin (angle (A,C,B));
A6: ((((|.(A - B).| * |.(B - C).|) * |.(C - A).|) * (sin (angle (A,C,B)))) / 2) / (the_area_of_polygon3 (B,C,A)) =
(((((|.(A - B).| * |.(B - C).|) * |.(C - A).|) * (sin (angle (A,C,B)))) * 1) / 2) * (1 / (the_area_of_polygon3 (B,C,A)))
by XCMPLX_1:99
.=
(((((|.(A - B).| * |.(B - C).|) * |.(C - A).|) * (1 / (the_area_of_polygon3 (B,C,A)))) * 1) / 2) * (sin (angle (A,C,B)))
.=
((((|.(A - B).| * |.(B - C).|) * |.(C - A).|) / (the_area_of_polygon3 (B,C,A))) / 2) * (sin (angle (A,C,B)))
by XCMPLX_1:99
;
(((|.(A - B).| * |.(B - C).|) * |.(C - A).|) / (the_area_of_polygon3 (B,C,A))) / 2 =
(((|.(A - B).| * |.(B - C).|) * |.(C - A).|) * (1 / (the_area_of_polygon3 (B,C,A)))) / 2
by XCMPLX_1:99
.=
(((|.(A - B).| * |.(B - C).|) * |.(C - A).|) / 2) * (1 / (the_area_of_polygon3 (B,C,A)))
.=
(((|.(A - B).| * |.(B - C).|) * |.(C - A).|) / 2) * (1 / (the_area_of_polygon3 (A,B,C)))
by Thm27
.=
(((|.(A - B).| * |.(B - C).|) * |.(C - A).|) / 2) / (the_area_of_polygon3 (A,B,C))
by XCMPLX_1:99
;
hence
|.(A - B).| = (the_diameter_of_the_circumcircle (A,B,C)) * (sin (angle (A,C,B)))
by A6, A5, EUCLID_6:43; verum