:: deftheorem Def11 defines DistEsti LATTICE5:def 11 :
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for b₄ being Cardinal holds
( b₄ = DistEsti d iff b₄, { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . (x,y) <= a "\/" b } are_equipotent );