theorem Th56:

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 &

PI < angle (

C,

B,

A) &

angle (

C,

B,

A)

< 2

* PI &

A in circle (

a,

b,

r) &

B in circle (

a,

b,

r) &

C in circle (

a,

b,

r) holds

the_diameter_of_the_circumcircle (

A,

B,

C)

= - (2 * r)