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 )