theorem Th11: :: CFDIFF_1:11
for X being Subset of COMPLEX st ( for z0 being Complex st z0 in X holds
ex N being Neighbourhood of z0 st N c= X ) holds
X is open