theorem Th7: :: LATTICE7:7

for L being non empty finite LATTICE
for x being Element of L holds height x >= 1