theorem :: CFDIFF_1:10

for X being Subset of COMPLEX st X is open holds
for z0 being Complex st z0 in X holds
ex g being Real st { y where y is Complex : |.(y - z0).| < g } c= X