for A being non empty set
for L being lower-bounded LATTICE
for d being distance_function of A,L holds succ {} c= DistEsti d