for L being non empty Poset
for x being Element of L holds
( ex_sup_of downarrow x,L & sup (downarrow x) = x )