theorem Th49:

for

a being

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).| )