theorem Th27: :: LATTICE5:27

for A being non empty set
for L being lower-bounded LATTICE
for O being Ordinal
for d being BiFunction of A,L
for q being QuadrSeq of d holds ConsecutiveDelta (q,(succ O)) = new_bi_fun ((BiFun ((ConsecutiveDelta (q,O)),(ConsecutiveSet (A,O)),L)),(Quadr (q,O)))