let A, B, C be Point of (TOP-REAL 2); ( A,B,C is_a_triangle implies the_diameter_of_the_circumcircle (A,B,C) = |.(C - A).| / (sin (angle (C,B,A))) )
assume
A,B,C is_a_triangle
; the_diameter_of_the_circumcircle (A,B,C) = |.(C - A).| / (sin (angle (C,B,A)))
then A2:
A,B,C are_mutually_distinct
by EUCLID_6:20;
the_diameter_of_the_circumcircle (A,B,C) =
(((|.(A - B).| * |.(B - C).|) * |.(C - A).|) / 2) / (((|.(A - B).| * |.(C - B).|) * (sin (angle (C,B,A)))) / 2)
by EUCLID_6:5
.=
(((|.(A - B).| * |.(B - C).|) * |.(C - A).|) / 2) / ((1 / 2) * ((|.(A - B).| * |.(C - B).|) * (sin (angle (C,B,A)))))
.=
((((|.(A - B).| * |.(B - C).|) * |.(C - A).|) / 2) / (1 / 2)) / (|.(A - B).| * (|.(C - B).| * (sin (angle (C,B,A)))))
by XCMPLX_1:78
.=
(((((|.(A - B).| * |.(B - C).|) * |.(C - A).|) / 2) / (1 / 2)) / |.(A - B).|) / (|.(C - B).| * (sin (angle (C,B,A))))
by XCMPLX_1:78
.=
(((|.(A - B).| * (|.(B - C).| * |.(C - A).|)) / |.(A - B).|) / |.(C - B).|) / (sin (angle (C,B,A)))
by XCMPLX_1:78
.=
((|.(B - C).| * |.(C - A).|) / |.(C - B).|) / (sin (angle (C,B,A)))
by XCMPLX_1:89, A2, EUCLID_6:42
.=
((|.(B - C).| * |.(C - A).|) / |.(B - C).|) / (sin (angle (C,B,A)))
by EUCLID_6:43
.=
|.(C - A).| / (sin (angle (C,B,A)))
by XCMPLX_1:89, A2, EUCLID_6:42
;
hence
the_diameter_of_the_circumcircle (A,B,C) = |.(C - A).| / (sin (angle (C,B,A)))
; verum