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