theorem :: SEQ_4:131

for n being Nat
for A being Subset of (COMPLEX n) holds
( A in ComplexOpenSets n iff A is open )