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