theorem :: LATTICE5:36

for A being non empty set
for L being lower-bounded LATTICE
for O being Ordinal
for d being distance_function of A,L
for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta (q,O) is distance_function of (ConsecutiveSet (A,O)),L by Th33, Th34, Th35;