theorem Th26: :: LATTICE5:26

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 holds ConsecutiveDelta (q,0) = d