theorem Th113: :: SEQ_4:114

for n being Nat
for x being Element of COMPLEX n
for A being Subset of (COMPLEX n) st A <> {} holds
dist (x,A) >= 0