:: deftheorem Def16 defines ConsecutiveDelta LATTICE5:def 16 :
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 O being Ordinal
for b₆ being set holds
( b₆ = ConsecutiveDelta (q,O) iff ex L0 being Sequence st
( b₆ = last L0 & dom L0 = succ O & L0 . 0 = d & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_bi_fun ((BiFun ((L0 . C),(ConsecutiveSet (A,C)),L)),(Quadr (q,C))) ) & ( for C being Ordinal st C in succ O & C <> 0 & C is limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) ) );