:: deftheorem Def2 defines Chain LATTICE7:def 2 :
for L being LATTICE
for x, y being Element of L st x <= y holds
for b₄ being non empty Chain of L holds
( b₄ is Chain of x,y iff ( x in b₄ & y in b₄ & ( for z being Element of L st z in b₄ holds
( x <= z & z <= y ) ) ) );