theorem Th20: :: LATTICE8:20

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
for T being Sequence
for O being Ordinal st O <> 0 & O is limit_ordinal & dom T = O & ( for O1 being Ordinal st O1 in O holds
T . O1 = ConsecutiveDelta2 (q,O1) ) holds
ConsecutiveDelta2 (q,O) = union (rng T)