for L1 being non empty up-complete Poset st L1 is finite holds
for x being Element of L1 holds x in compactbelow x