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) = - (the_diameter_of_the_circumcircle (B,A,C)) )
A3: ( |.(B - A).| = |.(A - B).| & |.(A - C).| = |.(C - A).| & |.(C - B).| = |.(B - C).| ) by EUCLID_6:43;
the_diameter_of_the_circumcircle (B,A,C) = (((|.(A - B).| * |.(C - A).|) * |.(B - C).|) / 2) / (- (the_area_of_polygon3 (A,B,C))) by A3, Thm28
.= - ((((|.(A - B).| * |.(C - A).|) * |.(B - C).|) / 2) / (the_area_of_polygon3 (A,B,C))) by XCMPLX_1:188 ;
hence ( A,B,C is_a_triangle implies the_diameter_of_the_circumcircle (A,B,C) = - (the_diameter_of_the_circumcircle (B,A,C)) ) ; :: thesis: verum