:: deftheorem Def13 defines QuadrSeq LATTICE5:def 13 :
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for b₄ being Sequence of [:A,A, the carrier of L, the carrier of L:] holds
( b₄ is QuadrSeq of d iff ( dom b₄ is Cardinal & b₄ is one-to-one & rng b₄ = { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . (x,y) <= a "\/" b } ) );