for L being non empty reflexive transitive RelStr
for X being Subset of L st ex_sup_of X,L holds
sup X = sup (downarrow X)