:: deftheorem defines open NCFCONT1:def 4 :
for CNS being ComplexNormSpace
for X being Subset of CNS holds
( X is open iff X ` is closed );