theorem Th9: :: LATTICE7:9

for L being finite LATTICE
for y being Element of L st y <> Bottom L holds
ex x being Element of L st x <(1) y