for F being non empty Poset
for A being Subset of F st A is finite & A <> {} & ( for B, C being Element of F st B in A & C in A & not B <= C holds
C <= B ) holds
ex m being Element of F st
( m in A & ( for C being Element of F st C in A holds
m <= C ) )