theorem :: YELLOW15:26

for L being non empty up-complete Poset st L is finite holds
the carrier of L = the carrier of (CompactSublatt L)