let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle implies ( the_radius_of_the_circumcircle (A,B,C) = |.((the_circumcenter (A,B,C)) - B).| & the_radius_of_the_circumcircle (A,B,C) = |.((the_circumcenter (A,B,C)) - C).| ) )
assume A1: A,B,C is_a_triangle ; :: thesis: ( the_radius_of_the_circumcircle (A,B,C) = |.((the_circumcenter (A,B,C)) - B).| & the_radius_of_the_circumcircle (A,B,C) = |.((the_circumcenter (A,B,C)) - C).| )
then ( |.((the_circumcenter (A,B,C)) - A).| = |.((the_circumcenter (A,B,C)) - B).| & |.((the_circumcenter (A,B,C)) - A).| = |.((the_circumcenter (A,B,C)) - C).| ) by Th50;
hence ( the_radius_of_the_circumcircle (A,B,C) = |.((the_circumcenter (A,B,C)) - B).| & the_radius_of_the_circumcircle (A,B,C) = |.((the_circumcenter (A,B,C)) - C).| ) by A1, Def4; :: thesis: verum