for L being with_infima Poset
for X being Subset of L holds
( X c= uparrow (fininfs X) & ( for F being Filter of L st X c= F holds
uparrow (fininfs X) c= F ) )