theorem Th1: :: LATTICE7:1

for L being LATTICE
for x, y being Element of L st x <= y holds
{x,y} is Chain of x,y