for L being with_infima Poset
for X being Subset of L st X is Open & X is lower holds
X is filtered