theorem Th41: :: TOPREAL9:43

for a, b, r being Real
for t being Point of (TOP-REAL 2) holds
( t in circle (a,b,r) iff |.(t - |[a,b]|).| = r )