for L being finite LATTICE
for a, b being Element of L st a < b holds
height a < height b