for X being Subset of COMPLEX holds
( X is open iff for x being Complex st x in X holds
ex N being Neighbourhood of x st N c= X ) by Th9, Th11;