let a be Real; :: thesis: for A, B, C being Point of (TOP-REAL 2)
for b, r being Real st A,B,C is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) holds
( |[a,b]| = the_circumcenter (A,B,C) & r = |.((the_circumcenter (A,B,C)) - A).| )
let A, B, C be Point of (TOP-REAL 2); :: thesis: for b, r being Real st A,B,C is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) holds
( |[a,b]| = the_circumcenter (A,B,C) & r = |.((the_circumcenter (A,B,C)) - A).| )
let b, r be Real; :: thesis: ( A,B,C is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) implies ( |[a,b]| = the_circumcenter (A,B,C) & r = |.((the_circumcenter (A,B,C)) - A).| ) )
assume that
A1: A,B,C is_a_triangle and
A2: A in circle (a,b,r) and
A3: B in circle (a,b,r) and
A4: C in circle (a,b,r) ; :: thesis: ( |[a,b]| = the_circumcenter (A,B,C) & r = |.((the_circumcenter (A,B,C)) - A).| )
A in { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = r } by A2, JGRAPH_6:def 5;
then consider Ar being Point of (TOP-REAL 2) such that
A5: Ar = A and
A6: |.(Ar - |[a,b]|).| = r ;
B in { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = r } by A3, JGRAPH_6:def 5;
then consider Br being Point of (TOP-REAL 2) such that
A7: Br = B and
A8: |.(Br - |[a,b]|).| = r ;
C in { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = r } by A4, JGRAPH_6:def 5;
then consider Cr being Point of (TOP-REAL 2) such that
A9: Cr = C and
A10: |.(Cr - |[a,b]|).| = r ;
A12: A,B,C are_mutually_distinct by A1, EUCLID_6:20;
A13: ( |.(A - |[a,b]|).| = |.(|[a,b]| - B).| & |.(B - |[a,b]|).| = |.(|[a,b]| - C).| & |.(C - |[a,b]|).| = |.(|[a,b]| - A).| ) by A5, A6, A7, A8, A9, A10, EUCLID_6:43;
( |[a,b]| in the_perpendicular_bisector (A,B) & |[a,b]| in the_perpendicular_bisector (B,C) & |[a,b]| in the_perpendicular_bisector (C,A) ) by A13, A12, EUCLID_6:43, Th45;
then A20: ( |[a,b]| in (the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) & |[a,b]| in (the_perpendicular_bisector (B,C)) /\ (the_perpendicular_bisector (C,A)) & |[a,b]| in (the_perpendicular_bisector (C,A)) /\ (the_perpendicular_bisector (A,B)) ) by XBOOLE_0:def 4;
( A,B,C is_a_triangle & B,C,A is_a_triangle & C,A,B is_a_triangle ) by A1, MENELAUS:15;
then ( {|[a,b]|} = (the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) & {|[a,b]|} = (the_perpendicular_bisector (B,C)) /\ (the_perpendicular_bisector (C,A)) & {|[a,b]|} = (the_perpendicular_bisector (C,A)) /\ (the_perpendicular_bisector (A,B)) ) by A20, Th17, Th46;
hence |[a,b]| = the_circumcenter (A,B,C) by A1, Def3; :: thesis: r = |.((the_circumcenter (A,B,C)) - A).|
hence r = |.((the_circumcenter (A,B,C)) - A).| by A5, A6, EUCLID_6:43; :: thesis: verum