theorem Th3: :: LATTICE7:3
for L being finite LATTICE
for C being Chain of L
for x, y being Element of L st x in C & y in C holds
( x < y iff height x < height y )