theorem Th8: :: LATTICE7:8

for L being finite LATTICE
for X being non empty Subset of L ex x being Element of L st
( x in X & ( for y being Element of L st y in X holds
not x < y ) )