:: deftheorem defines ComplexOpenSets SEQ_4:def 20 :
for n being Nat holds ComplexOpenSets n = { A where A is Subset of (COMPLEX n) : A is open } ;