for L being non empty complete Poset
for X being Subset of L
for p being Element of L st p is completely-irreducible & p = inf X holds
p in X