for L being non empty up-complete Poset st L is finite holds
for x being Element of L holds x is isolated_from_below