theorem :: CFDIFF_1:14

for X being Subset of COMPLEX
for z0 being Element of COMPLEX
for r being Real st X = { y where y is Complex : |.(y - z0).| <= r } holds
X is closed