theorem Th1: :: LATTICE8:1

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