theorem
:: EUCLID12:69
for
a
,
b
,
r
,
s
being
Real
st
r
<>
s
holds
circle
(
a
,
b
,
r
)
misses
circle
(
a
,
b
,
s
)