theorem :: LATTICE8:28

for A being non empty set
for L being lower-bounded modular LATTICE
for d being distance_function of A,L
for O being Ordinal
for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta2 (q,O) is distance_function of (ConsecutiveSet2 (A,O)),L by Th25, Th26, Th27;