theorem Th4: :: COMPLSP1:4

for n being Element of NAT
for V being Subset of (the_Complex_Space n)
for A being Subset of (COMPLEX n) st A = V holds
( A is open iff V is open ) by SEQ_4:131;