theorem Th23: :: JGRAPH_6:23

for a, b, r being Real
for Cb being Subset of (TOP-REAL 2) st r > 0 & Cb = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = r } holds
Cb is being_simple_closed_curve