let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle implies ( |.((the_circumcenter (A,B,C)) - A).| = |.((the_circumcenter (A,B,C)) - B).| & |.((the_circumcenter (A,B,C)) - A).| = |.((the_circumcenter (A,B,C)) - C).| & |.((the_circumcenter (A,B,C)) - B).| = |.((the_circumcenter (A,B,C)) - C).| ) )
assume A1: A,B,C is_a_triangle ; :: thesis: ( |.((the_circumcenter (A,B,C)) - A).| = |.((the_circumcenter (A,B,C)) - B).| & |.((the_circumcenter (A,B,C)) - A).| = |.((the_circumcenter (A,B,C)) - C).| & |.((the_circumcenter (A,B,C)) - B).| = |.((the_circumcenter (A,B,C)) - C).| )
then consider D being Point of (TOP-REAL 2) such that
A2: ( (the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) = {D} & (the_perpendicular_bisector (B,C)) /\ (the_perpendicular_bisector (C,A)) = {D} & (the_perpendicular_bisector (C,A)) /\ (the_perpendicular_bisector (A,B)) = {D} ) and
A3: ( |.(D - A).| = |.(D - B).| & |.(D - A).| = |.(D - C).| & |.(D - B).| = |.(D - C).| ) by Th47;
the_circumcenter (A,B,C) = D by A1, A2, Def3;
hence ( |.((the_circumcenter (A,B,C)) - A).| = |.((the_circumcenter (A,B,C)) - B).| & |.((the_circumcenter (A,B,C)) - A).| = |.((the_circumcenter (A,B,C)) - C).| & |.((the_circumcenter (A,B,C)) - B).| = |.((the_circumcenter (A,B,C)) - C).| ) by A3; :: thesis: verum