for A, B, C being Point of (TOP-REAL 2) holds the_diameter_of_the_circumcircle (A,B,C) = the_diameter_of_the_circumcircle (B,C,A) by Thm27;