theorem Th19: :: LATTICE8:19

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 holds ConsecutiveDelta2 (q,(succ O)) = new_bi_fun2 ((BiFun ((ConsecutiveDelta2 (q,O)),(ConsecutiveSet2 (A,O)),L)),(Quadr2 (q,O)))