theorem Th50: :: EUCLID12:66

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds
( |.((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).| )