theorem
Th48
:
:: EUCLID12:63
for
A
,
B
,
C
being
Point
of
(
TOP-REAL
2
)
st
A
,
B
,
C
is_a_triangle
holds
ex
a
,
b
,
r
being
Real
st
(
A
in
circle
(
a
,
b
,
r
) &
B
in
circle
(
a
,
b
,
r
) &
C
in
circle
(
a
,
b
,
r
) )