for L being with_infima Poset
for X being Subset of L st ( ex_inf_of X,L or L is complete ) holds
inf X = inf (fininfs X)