for L being non empty Poset
for D being non empty finite filtered Subset of L st ex_inf_of D,L holds
inf D in D