:: deftheorem Def3 defines the_circumcenter EUCLID12:def 5 :

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds

for b_{4} being Point of (TOP-REAL 2) holds

( b_{4} = the_circumcenter (A,B,C) iff ( (the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) = {b_{4}} & (the_perpendicular_bisector (B,C)) /\ (the_perpendicular_bisector (C,A)) = {b_{4}} & (the_perpendicular_bisector (C,A)) /\ (the_perpendicular_bisector (A,B)) = {b_{4}} ) );

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds

for b

( b