:: deftheorem defines the_diameter_of_the_circumcircle EUCLID10:def 1 :
for A, B, C being Point of (TOP-REAL 2) holds the_diameter_of_the_circumcircle (A,B,C) = (((|.(A - B).| * |.(B - C).|) * |.(C - A).|) / 2) / (the_area_of_polygon3 (A,B,C));