:: deftheorem Def17 defines dist SEQ_4:def 17 :
for n being Nat
for x being Element of COMPLEX n
for A being Subset of (COMPLEX n)
for b₄ being Real holds
( b₄ = dist (x,A) iff for X being Subset of REAL st X = { |.(x - z).| where z is Element of COMPLEX n : z in A } holds
b₄ = lower_bound X );