:: deftheorem Def21 defines BasicDF LATTICE5:def 21 :
for L being lower-bounded LATTICE
for b₂ being distance_function of the carrier of L,L holds
( b₂ = BasicDF L iff for x, y being Element of L holds
( ( x <> y implies b₂ . (x,y) = x "\/" y ) & ( x = y implies b₂ . (x,y) = Bottom L ) ) );