theorem Th55:
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 &
0 < angle (
C,
B,
A) &
angle (
C,
B,
A)
< 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