theorem Th20: :: JGRAPH_6:20

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