theorem Thm38: :: EUCLID10:58

for A, B being Point of (TOP-REAL 2)
for a, b being Real
for r being positive Real st A,B,|[a,b]| are_mutually_distinct & A in circle (a,b,r) & B in circle (a,b,r) & |[a,b]| in LSeg (A,B) holds
|.(A - B).| = 2 * r