theorem Th9: :: CFDIFF_1:9

for X being Subset of COMPLEX st X is open holds
for z0 being Complex st z0 in X holds
ex N being Neighbourhood of z0 st N c= X