theorem Th13: :: CFDIFF_1:13

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 open