theorem :: SEQ_4:122

for n being Nat
for r1 being Real
for A being Subset of (COMPLEX n) st A <> {} holds
Ball (A,r1) is open