for CNS being ComplexNormSpace
for x0 being Point of CNS
for N being Neighbourhood of x0 holds x0 in N