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