for L being non empty Poset holds
( L is with_infima iff for X being non empty finite Subset of L holds ex_inf_of X,L )