:: deftheorem defines NextSet LATTICE5:def 17 :
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L holds NextSet d = ConsecutiveSet (A,(DistEsti d));