theorem :: TOPREAL9:57

for a, b, r being Real
for s, t being Point of (TOP-REAL 2) st s <> t & s in closed_inside_of_circle (a,b,r) & t in closed_inside_of_circle (a,b,r) holds
r > 0