:: deftheorem Def1 defines dist JCT_MISC:def 1 :
for A, B being Subset of REAL
for b₃ being Real holds
( b₃ = dist (A,B) iff ex X being Subset of REAL st
( X = { |.(r - s).| where r, s is Real : ( r in A & s in B ) } & b₃ = lower_bound X ) );