theorem Th115: :: SEQ_4:116

for n being Nat
for x being Element of COMPLEX n
for A being Subset of (COMPLEX n) st x in A holds
dist (x,A) = 0