theorem
Th53
:
:: EUCLID12:72
for
A
,
B
,
C
being
Point
of
(
TOP-REAL
2
)
st
A
,
B
,
C
is_a_triangle
&
0
<
angle
(
C
,
B
,
A
) &
angle
(
C
,
B
,
A
)
<
PI
holds
the_diameter_of_the_circumcircle
(
A
,
B
,
C
)
>
0