for L being with_suprema Poset
for X being Subset of L holds
( X c= downarrow (finsups X) & ( for I being Ideal of L st X c= I holds
downarrow (finsups X) c= I ) )