theorem :: SEQ_4:132

for n being Nat
for A being Subset of (COMPLEX n) holds
( A is closed iff A ` is open )