theorem Th28: :: LATTICE5:28

for A being non empty set
for L being lower-bounded LATTICE
for T being Sequence
for O being Ordinal
for d being BiFunction of A,L
for q being QuadrSeq of d st O <> 0 & O is limit_ordinal & dom T = O & ( for O1 being Ordinal st O1 in O holds
T . O1 = ConsecutiveDelta (q,O1) ) holds
ConsecutiveDelta (q,O) = union (rng T)