theorem Th52:

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) & not

the_diameter_of_the_circumcircle (

A,

B,

C)

= 2

* r holds

the_diameter_of_the_circumcircle (

A,

B,

C)

= - (2 * r)