let a be Real; 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); 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; ( 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)
; ( |[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; r = |.((the_circumcenter (A,B,C)) - A).|
hence
r = |.((the_circumcenter (A,B,C)) - A).|
by A5, A6, EUCLID_6:43; verum