theorem :: EUCLID10:59

for a, b being Real
for r being positive Real
for C being Subset of (Euclid 2) st C = circle (a,b,r) holds
diameter C = 2 * r