for A being non empty set
for L being lower-bounded LATTICE
for d being distance_function of A,L holds DistEsti d <> {}