theorem :: SEQ_4:106

for n being Nat
for A being Subset of (COMPLEX n) st A = {} holds
A is open ;