:: 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₄ being Point of (TOP-REAL 2) holds
( b₄ = the_circumcenter (A,B,C) iff ( (the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) = {b₄} & (the_perpendicular_bisector (B,C)) /\ (the_perpendicular_bisector (C,A)) = {b₄} & (the_perpendicular_bisector (C,A)) /\ (the_perpendicular_bisector (A,B)) = {b₄} ) );