:: deftheorem defines NextDelta LATTICE5:def 18 :
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being QuadrSeq of d holds NextDelta q = ConsecutiveDelta (q,(DistEsti d));