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

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